Create a gist now

Instantly share code, notes, and snippets.

@gallais /Currying.v
Last active Aug 29, 2015

What would you like to do?
Currying using canonical structures
Require Import List.
Module Currying.
Record class (Dom : Type) (Curr : Type -> Type) :=
Class { Fun : forall cod, Curr cod -> (Dom -> cod) }.
Structure type := Pack { dom : Type
; curr : Type -> Type
; class_of : class dom curr }.
Definition flippedmap (Curry : type) :
forall cod, list (dom Curry) -> curr Curry cod -> list cod.
refine (let 'Pack _ _ (Class fc) := Curry
in fun cod xs f => List.map _ xs) ; apply fc, f.
Defined.
Arguments flippedmap {Curry} {cod} f xs.
Arguments Class {Dom} {Curr} Fun.
Module theory.
Notation "f <$> xs" := (flippedmap xs f) (at level 70).
End theory.
End Currying.
Import Currying.theory.
Definition pair_curry (c1 c2 : Currying.type) :
forall cod, Currying.curr c1 (Currying.curr c2 cod) ->
(Currying.dom c1 * Currying.dom c2) -> cod.
intros cod f (a, b).
apply c2 ; [| exact b].
apply c1 ; [| exact a].
exact f.
Defined.
Canonical Structure CurryingPair (c1 : Currying.type) (c2 : Currying.type) : Currying.type :=
Currying.Pack (Currying.dom c1 * Currying.dom c2)
(fun cod => Currying.curr c1 (Currying.curr c2 cod))
(Currying.Class (pair_curry c1 c2)).
Canonical Structure failsafe (a : Type) : Currying.type :=
Currying.Pack a (fun cod => a -> cod) (Currying.Class (fun _ f => f)).
Check ((fun x => 2 * x) <$> (cons 1 (cons 2 nil))).
Eval compute in ((fun x => 2 * x) <$> (cons 1 (cons 2 nil))).
Check ((fun x y => x) <$> (cons (1, 2) (cons (2, 3) nil))).
Eval compute in ((fun x y => x) <$> (cons (1, 2) (cons (2, 4) nil))).
Definition map_pair {A B C} (f : A -> B -> C) (l : list (A * B)) : list C := f <$> l.
Definition map_triple {A B C D} (f : A -> B -> C -> D) (l : list (A * B * C)) : list D := f <$> l.
Definition map_quad {A B C D E} (f : A -> B -> C -> D -> E) (l : list (A * B * C * D)) : list E := f <$> l.
Definition map_nestedpairs {A B C D E} (f : A -> B -> C -> D -> E) (l : list ((A * B) * (C * D))) : list E := f <$> l.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment