Fun with type functions
Friends GHC has embodied data type families since 6.8, and now type synonym families (aka type functions) in 6.10. However, apart from our initial papers there isn't much published material about how to *use* type families. But that hasn't stopped you: quite a few people are using them already, and of course there is a rich seam of work on using functional dependencies to express type-level computation. Ken Shan and Oleg Kiselyov and I are collaborating to write a paper for an upcoming workshop, under the general rubric of "Fun with type functions" (in homage to Thomas Hallgren's paper "Fun with functional dependencies" and Ralf Hinze's paper "Fun with phantom types"). So this message is to ask you: can you tell us about the most persuasive, fun application you've encountered, for type families or functional dependencies? Simple is good. It doesn't have to be elaborate: just something that does something useful you could not have done otherwise. Pointers to email threads are fine. Don't assume we already know about them (even if we participated in the thread :-) Part of what we're interested in is that *you* found the example compelling. Many thanks Simon, Ken, Oleg PS: I'm broadcasting this message to GHC-users and Haskell-cafe, but to avoid deluging ghc-users, please reply just to us and Haskell cafe. (Interested ghc-users can follow the threads there from the archives if they want.)
On Thu, Nov 27, 2008 at 9:29 AM, Simon Peyton-Jones
Friends
GHC has embodied data type families since 6.8, and now type synonym families (aka type functions) in 6.10. However, apart from our initial papers there isn't much published material about how to *use* type families. But that hasn't stopped you: quite a few people are using them already, and of course there is a rich seam of work on using functional dependencies to express type-level computation.
Ken Shan and Oleg Kiselyov and I are collaborating to write a paper for an upcoming workshop, under the general rubric of "Fun with type functions" (in homage to Thomas Hallgren's paper "Fun with functional dependencies" and Ralf Hinze's paper "Fun with phantom types").
So this message is to ask you:
can you tell us about the most persuasive, fun application you've encountered, for type families or functional dependencies?
Simple is good. It doesn't have to be elaborate: just something that does something useful you could not have done otherwise. Pointers to email threads are fine. Don't assume we already know about them (even if we participated in the thread :-) Part of what we're interested in is that *you* found the example compelling.
Many thanks
I documented, [1] and [2], my first encounter with functional dependencies. Maybe not a persuasive example, but I felt it was a fairly good introduction to them. /M [1]: http://therning.org/magnus/archives/354 [2]: http://therning.org/magnus/archives/355 -- Magnus Therning (OpenPGP: 0xAB4DFBA4) magnus＠therning．org Jabber: magnus＠therning．org http://therning.org/magnus identi.ca|twitter: magthe
On Thu, Nov 27, 2008 at 8:29 PM, Simon Peyton-Jones
So this message is to ask you:
can you tell us about the most persuasive, fun application you've encountered, for type families or functional dependencies?
I only just discovered functional dependencies a week or two ago, and when it solved my problem it absolutely made my day. I was reading 'Bananas, Lenses, etc.' and wanted to implement paramorphic recursion with a type class. My initial attempt: class Paramorphic p where term :: p -> Bool this :: p -> a next ::: p -> p para :: (Paramorphic p) => t -> (a -> (p, t) -> t) ->p -> t para a f p | term p = a | otherwise = f (this p) (next p, para a f (next p)) instance Paramorphic Int where term = (== 0) this = id next = subtract 1 This is broken, since 'a' in 'this' is loose. Then I found multiple class parameters: class Paramorphic p a where ... But 'a' was still too loose--para's type became para :: (Paramorphic p a, Paramorphic p a1, Paramorphic p a2, Paramorphic p a3) => t -> (a1 -> (p, t) -> t) -> p -> t But a fundep solved it for me: class Paramorphic p a | p -> a where ... I could now pretty much do factorial and tails from the paper. fact = para 1 (\a (_, b) -> a * b) instance Paramorphic [a] a where term = null this = head next = tail tails = para [[]] (\a (as, b) -> (a : as) : b) Not exactly a 'fun' example, but I was smiling for hours after discovering this. :) Toby.
My work on lightweight session types (modeled after this year's ICFP paper on the same subject) used type and data families extensively for an elegant way of connecting communicating coroutines: Empty types are used for sessions:
data Eps -- empty session data a :?: s -- read an "a" followed by session "s" data a :!: s -- write an "a" followed by session "s" -- etc.
These have kind *, which makes them easy to use in other type-level code; my first formulation had the session types as functors directly, but that led to needing kind signatures elsewhere and made working with these types much more difficult.. Type families are used to represent the dual of a session; that is, a session that reads an Int can connect with a session that writes an Int.
type family Dual s type instance Dual Eps = Eps type instance Dual (a :?: s) = a :!: Dual s type instance Dual (a :!: s) = a :?: Dual s -- etc.
Then data families give structure to the session:
data family Rep s a newtype instance Rep Eps a = Done a data instance Rep (x :!: s) a = Send x (Rep s a) newtype instance Rep (x :?: s) a = Receive (x -> Rep s a) -- etc.
Rep s converts a sessions (kind *) into a functor (kind * -> *). It also allows easy experimentation with alternate formulations of the problem that potentially have different kinds. Finally, a typeclass allows interpretation of these types, connecting two sessions together to run as coroutines:
class Coroutine s where connect :: (Dual s ~ c, Dual c ~ s) => Rep s a -> Rep c b -> (a,b)
instance Coroutine Eps where connect (Done a) (Done b) = (a,b) instance Coroutine s => Coroutine (x :!: s) where connect (Send x s) (Receive k) = connect s (k x) instance Coroutine s => Coroutine (x :?: s) where connect (Receive k) (Send x c) = connect (k x) c
The proof that two routines can safely connect is done entirely at
compile time; the connection routine just takes care of routing data
between the two processes.
-- ryan
On Thu, Nov 27, 2008 at 1:29 AM, Simon Peyton-Jones
Friends
GHC has embodied data type families since 6.8, and now type synonym families (aka type functions) in 6.10. However, apart from our initial papers there isn't much published material about how to *use* type families. But that hasn't stopped you: quite a few people are using them already, and of course there is a rich seam of work on using functional dependencies to express type-level computation.
Ken Shan and Oleg Kiselyov and I are collaborating to write a paper for an upcoming workshop, under the general rubric of "Fun with type functions" (in homage to Thomas Hallgren's paper "Fun with functional dependencies" and Ralf Hinze's paper "Fun with phantom types").
So this message is to ask you:
can you tell us about the most persuasive, fun application you've encountered, for type families or functional dependencies?
Simple is good. It doesn't have to be elaborate: just something that does something useful you could not have done otherwise. Pointers to email threads are fine. Don't assume we already know about them (even if we participated in the thread :-) Part of what we're interested in is that *you* found the example compelling.
Many thanks
Simon, Ken, Oleg
PS: I'm broadcasting this message to GHC-users and Haskell-cafe, but to avoid deluging ghc-users, please reply just to us and Haskell cafe. (Interested ghc-users can follow the threads there from the archives if they want.) _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Simon Peyton-Jones wrote:
can you tell us about the most persuasive, fun application you've encountered, for type families or functional dependencies?
I'm using them to provide witnesses to lenses. Given two lenses on the same base type, I want to compare them, and if they're the same lens, know that they have the same view type. data Lens base view = MkLens { -- lensWitness :: ???, lensGet :: base -> view, lensPut :: base -> view -> base }; How do I compare "Lens base view1" and "Lens base view2", and match up view1 and view2? The difficulty is that my witnesses are monomorphic, while a lens may be polymorphic. For instance, the lens corresponding to the "fst" function: fstLens :: Lens (a,b) a; fstLens = MkLens { lensGet = fst, lensPut = \(_,b) a -> (a,b) }; I only want to generate one open witness for fstLens, but what is its type? This is where type functions come in. I have a type family TF, and a basic set of instances: type family TF tf x; data TFIdentity; type instance TF TFIdentity x = x; data TFConst a; type instance TF (TFConst a) x = a; data TFApply (f :: * -> *); type instance TF (TFApply f) x = f x; data TFMatch; type instance TF TFMatch (f a) = a; data TFMatch1; type instance TF TFMatch1 (f a b) = a; data TFCompose tf1 tf2; type instance TF (TFCompose tf1 tf2) x = TF tf1 (TF tf2 x); I create a new witness type, that witnesses type functions: import Data.Witness; data TFWitness w x y where { MkTFWitness :: w tf -> TFWitness w x (TF tf x); }; instance (SimpleWitness w) => SimpleWitness (TFWitness w x) where { matchWitness (MkTFWitness wtf1) (MkTFWitness wtf2) = do { MkEqualType <- matchWitness wtf1 wtf2; return MkEqualType; }; }; So for my lens type, I want a witness for the type function from base to view: data Lens base view = MkLens { lensWitness :: TFWitness IOWitness base view, lensGet :: base -> view, lensPut :: base -> view -> base }; For our "fst" lens, I can now generate a witness for the function from "(a,b)" to "a". fstWitness :: IOWitness TFMatch1; fstWitness <- newIOWitness; -- language extension fstLens :: Lens (a,b) a; fstLens = MkLens { lensWitness = MkTFWitness fstWitness, lensGet = fst, lensPut = \(_,b) a -> (a,b) }; I can now compare two lenses like this: get1put2 :: Lens base view1 -> Lens base view2 -> base -> Maybe base; get1put2 lens1 lens2 b = do { MkEqualType <- matchWitness (lensWitness lens1) (lensWitness lens2); return (lensPut lens2 b (lensGet lens1 b)); }; (Actually, I'm doing something a bit more useful than get1put2.) -- Ashley Yakeley
2008/11/27 Simon Peyton-Jones
can you tell us about the most persuasive, fun application you've encountered, for type families or functional dependencies?
Hi, I certainly had fun with the Instant Insanity puzzle, in Monad.Reader issue 8: http://www.haskell.org/haskellwiki/User:ConradParker/InstantInsanity That was using functional dependencies. Then Pepe Iborra pasted a version of Instant Insanity with type families: http://hpaste.org/2689 Looking back at this, Manuel left the following comment: -- There is unfortunately, no simple way to print the normalised type. -- In fact, GHC goes to great length to show types with as little -- normalisation as possible to users. (Especially for error messages, -- that usually makes them much easier to understand.) However, with -- type families, I think we really ought to have a ghci command to -- specifically request a normalised type. I'll put that on my -- TODO list! -- For the moment, you can of course try forcing normalisation by -- triggering type errors; eg -- > :t solution :: Int (Does ghci now have a command for printing normalised types?) There are also links to haskell-cafe discussion and some other implementations (in C++ templates and D) to, um, compare: http://www.haskell.org/haskellwiki/User_talk:ConradParker/InstantInsanity cheers, Conrad.
Pointless Haskell a library for point-free programming with recursion patterns that uses type synonym families to provide a view of data types as the fixed points of functors. It defines two type functions type family PF a :: * -> * -- returns the pattern functor for a data type type family Rep (f :: * -> *) x :: * -- returns the result type of applying a functor to a type argument that can be combined to derive the structurally equivalent sum of products for some type: type F a x = Rep (PF a) x class Mu a where inn :: F a a -> a out :: a -> F a a For Haskell polymorphic lists, we need to define: type instance PF [a] = Const One :+: Const a :*: Id instance Mu [a] where inn (Left _) = [] inn (Right (x,xs)) = x:xs out [] = Left _L out (x:xs) = Right (x,xs) Some of the typical recursion patterns are: hylo :: Functor (PF b) => b -> (F b c -> c) -> (a -> F b a) -> a -> c cata :: (Mu a,Functor (PF a)) => a -> (F a b -> b) -> a -> b ana :: (Mu b,Functor (PF b)) => b -> (a -> F b a) -> a -> b One simple example is the foldr (catamorphism) for calculating the lenght of a list: length :: [a] -> Int length = cata (_L::[a]) f where f = zero \/ succ . snd
length [1,2,3,4] 4
I have promoted the library into a cabal package (pointless-haskell) today
and am creating an homepage (
http://haskell.di.uminho.pt/wiki/Pointless+Haskell) with examples.
cheers,
hugo
On Thu, Nov 27, 2008 at 9:29 AM, Simon Peyton-Jones
Friends
GHC has embodied data type families since 6.8, and now type synonym families (aka type functions) in 6.10. However, apart from our initial papers there isn't much published material about how to *use* type families. But that hasn't stopped you: quite a few people are using them already, and of course there is a rich seam of work on using functional dependencies to express type-level computation.
Ken Shan and Oleg Kiselyov and I are collaborating to write a paper for an upcoming workshop, under the general rubric of "Fun with type functions" (in homage to Thomas Hallgren's paper "Fun with functional dependencies" and Ralf Hinze's paper "Fun with phantom types").
So this message is to ask you:
can you tell us about the most persuasive, fun application you've encountered, for type families or functional dependencies?
Simple is good. It doesn't have to be elaborate: just something that does something useful you could not have done otherwise. Pointers to email threads are fine. Don't assume we already know about them (even if we participated in the thread :-) Part of what we're interested in is that *you* found the example compelling.
Many thanks
Simon, Ken, Oleg
PS: I'm broadcasting this message to GHC-users and Haskell-cafe, but to avoid deluging ghc-users, please reply just to us and Haskell cafe. (Interested ghc-users can follow the threads there from the archives if they want.) _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
-- www.di.uminho.pt/~hpacheco
participants (7)
-
Ashley Yakeley -
Conrad Parker -
Hugo Pacheco -
Magnus Therning -
Ryan Ingram -
Simon Peyton-Jones -
Toby Hutton