(* -*- proof-three-window-mode-policy: hybrid -*- *)
(** A Limited Case for Reification by Type Inference *)
(** By Jason Gross *)
(** Outline:
1. Goal:
Perform some operation which requires a structured
representation of curried types, e.g., reversal
2. notation for reified currying + operation
3. notation for normal currying
4. implementation of normal currying notation
5. implementation of reified currying
(6. implementation of reversal *)
(***************************************************************)
(** 1. Goal: Perform some operation which requires a structured
representation of curried types, e.g., reversal *)
(** 2. notation for reified currying + operation *)
(**
<<
Notation "'->uncurryR' x , .. , y => v" := ⋯
Eval cbv -["+"] in
rev_uncurry (->uncurryR x, y, z, w => x + y + z + w).
(* = fun '(v2, a1, a0, a) => a + a0 + a1 + v2 *)
>> *)
(** 3. notation for normal currying *)
(**
<<
Notation "'->uncurry' x , .. , y => v" := ⋯ .
>> *)
(** 4. implementation of normal currying notation *)
Definition uncurry2 {A B C} (f : A -> B -> C) : A * B -> C
:= fun '(a, b) => f a b.
Check uncurry2 Nat.add. (* uncurry2 Nat.add : nat * nat -> nat *)
Eval cbv [uncurry2] in uncurry2 Nat.add.
(* = fun '(a, b) => a + b
: nat * nat -> nat
*)
Eval cbv [uncurry2] in
uncurry2 (fun a b c d e => a + b + c + d + e).
(* = fun '(a, b) (c d e : nat) => a + b + c + d + e
: nat * nat -> nat -> nat -> nat -> nat *)
Notation "'->uncurry3' x , y , z => v" :=
(uncurry2 (fun x => uncurry2 (fun y => (fun z => v))))
(at level 200, v at level 100, only parsing).
Check ->uncurry3 x, y, z => x + y + z.
Eval cbv -["+"] in ->uncurry3 x, y, z => x + y + z.
Notation "'->uncurry3' x , y , z => v" :=
(uncurry2 (fun x => uncurry2 (fun y => uncurry2 (fun z (_ : unit) => v))))
(at level 200, v at level 100, only parsing).
Check ->uncurry3 x, y, z => x + y + z.
Eval cbv -["+"] in ->uncurry3 x, y, z => x + y + z.
Notation "'->uncurry' x , .. , y => v" :=
(uncurry2 (fun x => .. (uncurry2 (fun y (_ : unit) => v)) .. ))
(at level 200, x closed binder, y closed binder,
v at level 100, only parsing).
Check ->uncurry x, y, z, w => x + y + z + w.
Eval cbv [uncurry2] in ->uncurry x, y, z, w => x + y + z + w.
(***************************************************************)
(* 5. implementation of reified currying *)
Inductive uncurry_types :=
| ccons (A : Type) (rest : uncurry_types) | cnil.
Fixpoint denoteUncurried (A : uncurry_types) : Type :=
match A with
| cnil => unit
| ccons A As => A * denoteUncurried As
end.
Eval cbv [denoteUncurried] in
denoteUncurried (ccons nat (ccons bool (ccons Set cnil))).
Definition uncurry {A As B} (f : A -> denoteUncurried As -> B)
: denoteUncurried (ccons A As) -> B
:= fun '(a, b) => f a b.
Notation "'->uncurryR' x , .. , y => v" :=
(uncurry (fun x => .. (uncurry (fun y (_ : unit) => v)) .. ))
(at level 200, x closed binder, y closed binder,
v at level 100, only parsing).
Fail Eval cbv [uncurry] in ->uncurryR x, y, z, w => x + y + z + w.
(* The command has indeed failed with message:
Found type "unit" where "denoteUncurried ?As2" was expected.
*)
Notation "'->uncurryR' x , .. , y => v" :=
(uncurry (fun x => .. (uncurry (fun y (_ : denoteUncurried cnil) => v)) .. ))
(at level 200, x closed binder, y closed binder,
v at level 100, only parsing).
Eval cbv [uncurry] in ->uncurryR x, y, z, w => x + y + z + w.
(* = fun '(a, (a0, (a1, (a2, _)))) => a + a0 + a1 + a2
: denoteUncurried (ccons nat (ccons nat (ccons nat (ccons nat cnil)))) -> nat
*)
(***************************************************************)
(* (6. implementation of reversal *)
(* Example of a cool thing to be done: reversing uncurrying *)
Fixpoint denoteUncurried_rev (A : uncurry_types) : Type
:= match A with
| cnil => unit
| ccons A As => denoteUncurried_rev As * A
end.
Fixpoint uncurry_rev (A : uncurry_types)
: denoteUncurried_rev A -> denoteUncurried A
:= match A with
| cnil => fun v => v
| ccons A As => fun '(v, a) => (a, uncurry_rev As v)
end.
Definition rev_uncurry {A B} (f : denoteUncurried A -> B)
: denoteUncurried_rev A -> B
:= fun v => f (uncurry_rev _ v).
Eval cbv -["+"] in rev_uncurry (->uncurryR x, y, z, w => x + y + z + w).
(* = fun v : unit * nat * nat * nat * nat =>
let
'(a, (a0, (a1, (a2, _)))) :=
let
'(v0, a) := v in
(a,
let
'(v1, a0) := v0 in
(a0,
let
'(v2, a1) := v1 in
(a1, let '(v3, a2) := v2 in (a2, v3)))) in
a + a0 + a1 + a2
: denoteUncurried_rev
(ccons nat (ccons nat (ccons nat (ccons nat cnil)))) ->
nat
*)
Fixpoint denoteUncurried_rev_nounit (A : uncurry_types) : Type
:= match A with
| cnil => unit
| ccons A cnil => A
| ccons A As => denoteUncurried_rev_nounit As * A
end.
Fixpoint uncurry_rev_cps {T} (A : uncurry_types)
: denoteUncurried_rev_nounit A -> (denoteUncurried A -> T) -> T
:= match A with
| cnil => fun v k => k v
| ccons A As
=> match As return (denoteUncurried_rev_nounit As -> (denoteUncurried As -> T) -> T) -> denoteUncurried_rev_nounit (ccons A As) -> _ with
| cnil => fun _ v k => k (v, tt)
| _ => fun uncurry_rev_cps v k
=> let '(v, a) := v in
uncurry_rev_cps v (fun v => k (a, v))
end (uncurry_rev_cps As)
end.
Definition rev_uncurry_by_cps {A B} (f : denoteUncurried A -> B)
: denoteUncurried_rev_nounit A -> B
:= fun v => uncurry_rev_cps _ v f.
Eval cbv -["+"] in
rev_uncurry_by_cps (->uncurryR x, y, z, w => x + y + z + w).
(* = fun '(v2, a1, a0, a) => a + a0 + a1 + v2
: denoteUncurried_rev_nounit
(ccons nat (ccons nat (ccons nat (ccons nat cnil)))) ->
nat
*)