[Haskell-cafe] Partial type family application

[Jan Stolarek]

mniip, you might want to take a look at a paper Richard Eisenberg and I wrote together in 2014:

Eisenberg, R. A., and Stolarek, J.: Promoting Functions to Type Families in Haskell, ACM SIGPLAN 
Notices 49(12):95-106 (originally published at: Haskell Symposium 2014, Göteborg, Sweden)

Janek


Dnia środa, 26 kwietnia 2017, mniip napisał:
> Oops, got cut off :S
>
> We could then write stuff like
>
>     type family Foldr (f :: k ~> l ~> l) (z :: l) (xs :: [k]) :: l where
>         Foldr f z '[] = z
>         Foldr f z (x ': xs) = f x (Foldr f z xs)
>
>     type family Flip (f :: k ~> l ~> m) (x :: l) (y :: k) :: m where
>         Flip f x y = f y x
>
>     -- Lift a type constructor into a type family
>     type family Apply (con :: k -> l) (x :: k) :: l where
>         Apply con x = con x
>
>     type family (.) (f :: l ~> m) (g :: k ~> l) (x :: k) :: l where
>         (.) f g x = f (g x)
>
>     stuff :: Foldr (Flip (Apply . Apply (,))) () '[Int, String, Char]
>     stuff = ((((), 'x'), "moo"), 3)
>
> This idea is very fresh, and I certainly haven't explored all the
> aspects, so I would welcome constructive (and intuitionistic) criticism
> regarding both usefulness and mathematical soundness of this.
>
> --mniip
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.


 

--- 
Politechnika Łódzka 
Lodz University of Technology 

Treść tej wiadomości zawiera informacje przeznaczone tylko dla adresata. 
Jeżeli nie jesteście Państwo jej adresatem, bądź otrzymaliście ją przez pomyłkę 
prosimy o powiadomienie o tym nadawcy oraz trwałe jej usunięcie. 

This email contains information intended solely for the use of the individual to whom it is addressed. 
If you are not the intended recipient or if you have received this message in error, 
please notify the sender and delete it from your system.