Safe lists with GADT's
Hi I'm starting to play with GADT's, and I was trying to write a safe version of head and tail, on a safe version of lists. What I came up with is:
data ConsT a data NilT
data List a t where Cons :: a -> List a b -> List a (ConsT b) Nil :: List a NilT
instance Show a => Show (List a t) where show (Cons a b) = show a ++ ":" ++ show b show Nil = "[]"
safeHead :: List a (ConsT t) -> a safeHead (Cons a b) = a
safeTail :: List a (ConsT t) -> List a t safeTail (Cons a b) = b
safeMap :: (a -> b) -> List a t -> List b t safeMap f Nil = Nil safeMap f (Cons a b) = Cons (f a) (safeMap f b)
Defining safeMap was trivial, but one thing I couldn't figure out was how to write something like fromList: fromList [] = Nil fromList (a:as) = Cons a (fromList as) fromList could obviously be anything such as reading from a file etc, where the input is not known in advance. Are there any techniques for this? In addition I was expecting to find some example like this in one of the papers/examples on GADT's, but I didn't. The Haskell wikibook has a slight example along these lines, but not with the recursive field in ConsT. [http://en.wikibooks.org/wiki/Haskell/GADT] Any help or hints would be appreciated, Thanks Neil
On Sun, Feb 25, 2007 at 10:40:13PM +0000, Neil Mitchell wrote:
Hi
I'm starting to play with GADT's, and I was trying to write a safe version of head and tail, on a safe version of lists. What I came up with is:
[code moved later]
Defining safeMap was trivial, but one thing I couldn't figure out was how to write something like fromList:
fromList [] = Nil fromList (a:as) = Cons a (fromList as)
fromList could obviously be anything such as reading from a file etc, where the input is not known in advance. Are there any techniques for this?
In addition I was expecting to find some example like this in one of the papers/examples on GADT's, but I didn't. The Haskell wikibook has a slight example along these lines, but not with the recursive field in ConsT. [http://en.wikibooks.org/wiki/Haskell/GADT]
Since we don't know in advance the length of the list, we need an existensial type; this immediately causes problems because existential types do not exist in any current Haskell implementation. There are two approaches: \begin{code} data ConsT a data NilT data List a t where Cons :: a -> List a b -> List a (ConsT b) Nil :: List a NilT instance Show a => Show (List a t) where show (Cons a b) = show a ++ ":" ++ show b show Nil = "[]" safeHead :: List a (ConsT t) -> a safeHead (Cons a b) = a safeTail :: List a (ConsT t) -> List a t safeTail (Cons a b) = b safeMap :: (a -> b) -> List a t -> List b t safeMap f Nil = Nil safeMap f (Cons a b) = Cons (f a) (safeMap f b) -- Using an existential datatype box data VarList a = forall t. VarList (List a t) fromListV :: [a] -> VarList a fromListV [] = VarList Nil fromListV (x:xs) = case fromListV xs of VarList xs' -> VarList (Cons x xs') -- using CPS transform (turns existentials into rank2) -- generally prefered because it avoids naming a one-use data type, -- but YMMV fromListC :: [a] -> (forall t. List a t -> r) -> r fromListC [] fn = fn Nil fromListC (x:xs) fn = fromListC xs (\sl -> fn (Cons x sl)) \end{code} HTH Stefan
Hi Stefan,
Since we don't know in advance the length of the list, we need an existensial type; this immediately causes problems because existential types do not exist in any current Haskell implementation. There are two approaches:
-- Using an existential datatype box data VarList a = forall t. VarList (List a t)
fromListV :: [a] -> VarList a fromListV [] = VarList Nil fromListV (x:xs) = case fromListV xs of VarList xs' -> VarList (Cons x xs')
-- using CPS transform (turns existentials into rank2) -- generally prefered because it avoids naming a one-use data type, -- but YMMV
fromListC :: [a] -> (forall t. List a t -> r) -> r fromListC [] fn = fn Nil fromListC (x:xs) fn = fromListC xs (\sl -> fn (Cons x sl))
How do I get my original function back which just turns a standard list to one of the funky lists, or is that just impossible with GADT's? Do I now have to "wrap" all the fuctions I use, i.e. pass safeMap in CPS? Thanks Neil
On Sun, Feb 25, 2007 at 11:11:14PM +0000, Neil Mitchell wrote:
Hi Stefan,
Since we don't know in advance the length of the list, we need an existensial type; this immediately causes problems because existential types do not exist in any current Haskell implementation. There are two approaches:
-- Using an existential datatype box data VarList a = forall t. VarList (List a t)
fromListV :: [a] -> VarList a fromListV [] = VarList Nil fromListV (x:xs) = case fromListV xs of VarList xs' -> VarList (Cons x xs')
-- using CPS transform (turns existentials into rank2) -- generally prefered because it avoids naming a one-use data type, -- but YMMV
fromListC :: [a] -> (forall t. List a t -> r) -> r fromListC [] fn = fn Nil fromListC (x:xs) fn = fromListC xs (\sl -> fn (Cons x sl))
How do I get my original function back which just turns a standard list to one of the funky lists, or is that just impossible with GADT's? Do I now have to "wrap" all the fuctions I use, i.e. pass safeMap in CPS?
AFAIK you can't. Fortunately the CPS transform can be very local: -- write this as you normally would, no cps at all do_something_with_safe_list :: List t a -> (something -> somethingelse ...) --assoc for clarity do_something_with_unsafe_list :: [a] -> (same as above) do_something_with_unsafe_list ls = fromListC ls do_something_with_safe_list
Stefan O'Rear wrote:
How do I get my original function back which just turns a standard list to one of the funky lists, or is that just impossible with GADT's? Do I now have to "wrap" all the fuctions I use, i.e. pass safeMap in CPS?
AFAIK you can't. Fortunately the CPS transform can be very local:
Indeed, you can't. I mean, given fromList [] = Nil fromList (a:as) = Cons a (fromList as) what type would it have? One of fromList :: forall t . [a] -> List a t fromList :: [a] -> List a NilT fromList :: forall t . [a] -> List a (ConsT t) ? No, because the second argument depends on the input list. The only thing we know is that there is a type t but we don't know which one. Thus fromList :: [a] -> (exists t . List a t) is the correct type. As Haskell currently doesn't have "first class existentials", we have to either pack it into a data type or appeal to the equivalence exists a . f a ~= forall r . (forall a . f a -> r) -> r Both have of course the problem that we cannot simply write safeMap (fromList [1,2,3]) :: exists t . List a t Regards, apfelmus Exercise: Why is fromList :: exists t . [a] -> List a t wrong as well?
Neil Mitchell wrote:
data ConsT a data NilT
data List a t where Cons :: a -> List a b -> List a (ConsT b) Nil :: List a NilT
Stefan O'Rear wrote:
data VarList a = forall t. VarList (List a t)
fromListV :: [a] -> VarList a fromListV [] = VarList Nil fromListV (x:xs) = case fromListV xs of VarList xs' -> VarList (Cons x xs')
fromListC :: [a] -> (forall t. List a t -> r) -> r fromListC [] fn = fn Nil fromListC (x:xs) fn = fromListC xs (\sl -> fn (Cons x sl))
I noticed that fromListV and fromListC always force traversal of the input list. I made various attempts to modify them to preserve laziness, but this always resulted in a type error. For example:
fromListV (x:xs) = case fromListV xs of ~(VarList l) -> VarList (Cons x l)
Couldn't match the rigid variable `a' against the rigid variable `a1' `a' is bound by the type signature for `fromListV' `a1' is bound by the pattern for `VarList' at gadt-list.hs:33:42-50 Expected type: List a b Inferred type: List a1 t In the second argument of `Cons', namely `l' In the first argument of `VarList', namely `(Cons x l)' I guess the strict traversal of the input list is inevitable, considering that the concrete type of any (List a t) depends on the length of the list (even when hidden behind an existential).
On Mon, Feb 26, 2007 at 03:42:56PM +1000, Matthew Brecknell wrote:
Neil Mitchell wrote:
data ConsT a data NilT
data List a t where Cons :: a -> List a b -> List a (ConsT b) Nil :: List a NilT
Stefan O'Rear wrote:
data VarList a = forall t. VarList (List a t)
fromListV :: [a] -> VarList a fromListV [] = VarList Nil fromListV (x:xs) = case fromListV xs of VarList xs' -> VarList (Cons x xs')
fromListC :: [a] -> (forall t. List a t -> r) -> r fromListC [] fn = fn Nil fromListC (x:xs) fn = fromListC xs (\sl -> fn (Cons x sl))
I noticed that fromListV and fromListC always force traversal of the input list. I made various attempts to modify them to preserve laziness, but this always resulted in a type error. For example:
fromListV (x:xs) = case fromListV xs of ~(VarList l) -> VarList (Cons x l)
Couldn't match the rigid variable `a' against the rigid variable `a1' `a' is bound by the type signature for `fromListV' `a1' is bound by the pattern for `VarList' at gadt-list.hs:33:42-50 Expected type: List a b Inferred type: List a1 t In the second argument of `Cons', namely `l' In the first argument of `VarList', namely `(Cons x l)'
I guess the strict traversal of the input list is inevitable, considering that the concrete type of any (List a t) depends on the length of the list (even when hidden behind an existential).
I can't find it now, but there was a post saying this couldn't be done because system fc is strict in type arguments, such as bound by forall t.
Neil Mitchell wrote:
Hi
I'm starting to play with GADT's, and I was trying to write a safe version of head and tail, on a safe version of lists. What I came up with is:
data ConsT a data NilT
data List a t where Cons :: a -> List a b -> List a (ConsT b) Nil :: List a NilT
instance Show a => Show (List a t) where show (Cons a b) = show a ++ ":" ++ show b show Nil = "[]"
safeHead :: List a (ConsT t) -> a safeHead (Cons a b) = a
safeTail :: List a (ConsT t) -> List a t safeTail (Cons a b) = b
safeMap :: (a -> b) -> List a t -> List b t safeMap f Nil = Nil safeMap f (Cons a b) = Cons (f a) (safeMap f b)
Defining safeMap was trivial, but one thing I couldn't figure out was how to write something like fromList:
fromList [] = Nil fromList (a:as) = Cons a (fromList as)
You need to use existentials. The following code hides one in its definition: fromList :: [a] -> (List a NilT -> r) -> (forall b. List a (ConsT b) -> r) -> r fromList [] nilk consk = nilk Nil fromList (x:xs) nilk consk = fromList' xs (consk . Cons x) where fromList' :: [a] -> (forall b. List a b -> r) -> r fromList' [] k = k Nil fromList' (x:xs) k = fromList' xs (k . Cons x) Also it should be possible to arrange this to use a very simple library for existentials I made, made possible by GHC 6.6's new support for impredicativity. -- exists a. F a -- <=> exists a.not (not (F a)) -- <=> not (forall a.not (F a)) type Exists f = forall r.(forall a.(f a -> r)) -> r open :: Exists f -> (forall a.(f a -> r)) -> r open package k = package k pack :: f a -> Exists f pack a k = k a
On Sun, Feb 25, 2007 at 10:40:13PM +0000, Neil Mitchell wrote:
data ConsT a data NilT
data List a t where Cons :: a -> List a b -> List a (ConsT b) Nil :: List a NilT ... Defining safeMap was trivial, but one thing I couldn't figure out was how to write something like fromList:
fromList [] = Nil fromList (a:as) = Cons a (fromList as)
fromList could obviously be anything such as reading from a file etc, where the input is not known in advance. Are there any techniques for this?
My favorite ways to wrap an existential is with another GADT: data Existential a where Existential :: a b -> a (Yes, properly speaking this isn't a GADT, just an existential ADT, but it's easier for me to understand this way.) Then fromList [] = Existential Nil fromList (a:as) = case fromList as of Existential as' -> Existential (Cons a as') This is a pretty easy way to deal with the fromList. You'll now also want (which I don't think you mentioned in your example code) a GADT version of null, and perhaps other length operators: data NullT t where IsNull :: NullT NilT NotNull :: NullT (ConsT t) nullL :: List a t -> NullT t so you can now actually use your head function on a dynamically generated list, by running something like (e.g. in a monad) do cs <- readFile "foo" Existential cs' <- return $ fromList cs -- note: we'll pattern-match fail on non-empty list here, which -- may not gain much, we'd use case statements in reality, or we'd -- catch failure within the monad, which is also safe--provided you -- catch them, which the language doesn't force you to do! (Or if -- we're in a pure monad like Maybe.) NotNull <- nullL cs' let c = headL cs' t = tailL cs' -- Now to illustrate the power of the GADT, a line that will fail -- at compile time: t' = tailL t return c -- David Roundy http://www.darcs.net
I am really curious about this style of programming, and find myself playing with it from time to time. The example so far is very nice, but the funniest part is missing. That is, defining appendL.
appendL :: List a t1 -> List a t2 -> List a t3
This says that the append of a list of length t1 and a list of length t2 is a list of whatever length t3 we want. Obviously this is not true and will not typecheck. After some healthy days of reading papers and theses, I've found at least three ways of defining it. First, via existentials:
appendL1 :: List a t1 -> List a t2 -> exists t3. List a t3
Second, attaching a proof. Question: what would be the advantage of the proof here?
data Add a b c where Base :: Add NilT a a ; Step :: Add a b c -> Add (ConsT a) b (ConsT c) appendL2 :: List a t1 -> List a t2 -> exists t3. (Add t1 t2 t3, List a t3)
Third, via Type Classes. \begin{code} class AddList a b c | a b -> c where append :: List x a -> List x b -> List x c instance AddList NilT b b where append Nil x = x instance AddList a b c => AddList (ConsT a) b (ConsT c) where append (Cons x l) l' = Cons x (append l l') \end{code} Given the three methods, I wouldn't know which one should be preferred, and why. In the first one you pay the burden of programming with existentials. The second one in addition to that is the least efficient, as building the proof surely has a cost. Since we are building it, isn't there a way to use it to remove the existential? Finally, with the third one your compiler will produce error messages that will make you swear, apart from possible efficiency losses too. Thanks for reading, any hints will be appreciated pepe On 26/02/2007, at 15:26, David Roundy wrote:
On Sun, Feb 25, 2007 at 10:40:13PM +0000, Neil Mitchell wrote:
data ConsT a data NilT
data List a t where Cons :: a -> List a b -> List a (ConsT b) Nil :: List a NilT ... Defining safeMap was trivial, but one thing I couldn't figure out was how to write something like fromList:
fromList [] = Nil fromList (a:as) = Cons a (fromList as)
fromList could obviously be anything such as reading from a file etc, where the input is not known in advance. Are there any techniques for this?
My favorite ways to wrap an existential is with another GADT:
data Existential a where Existential :: a b -> a
(Yes, properly speaking this isn't a GADT, just an existential ADT, but it's easier for me to understand this way.)
Then
fromList [] = Existential Nil fromList (a:as) = case fromList as of Existential as' -> Existential (Cons a as')
This is a pretty easy way to deal with the fromList. You'll now also want (which I don't think you mentioned in your example code) a GADT version of null, and perhaps other length operators:
data NullT t where IsNull :: NullT NilT NotNull :: NullT (ConsT t)
nullL :: List a t -> NullT t
so you can now actually use your head function on a dynamically generated list, by running something like (e.g. in a monad)
do cs <- readFile "foo" Existential cs' <- return $ fromList cs -- note: we'll pattern-match fail on non-empty list here, which -- may not gain much, we'd use case statements in reality, or we'd -- catch failure within the monad, which is also safe-- provided you -- catch them, which the language doesn't force you to do! (Or if -- we're in a pure monad like Maybe.) NotNull <- nullL cs' let c = headL cs' t = tailL cs' -- Now to illustrate the power of the GADT, a line that will fail -- at compile time: t' = tailL t return c
-- David Roundy http://www.darcs.net _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On Mon, Feb 26, 2007 at 04:35:06PM +0100, Pepe Iborra wrote:
First, via existentials:
appendL1 :: List a t1 -> List a t2 -> exists t3. List a t3
It seems like this problem is begging for the new indexed types (for which I never remember the right syntax). type AddListTs :: * -> * -> * AddListTs NilT NilT = NilT AddListTs NilT t = t AddListTs (ConsT t) t' = AddListTs t (ConsT t') then appendLi :: List a t1 -> List a t2 -> List a (AddListTs t1 t2) I'd be interested if Manuel had an idea whether this would work right. I think it can be made equivalent to the FD approach, but doesn't require that you define a "stupid" class, and is far, far prettier. -- David Roundy Department of Physics Oregon State University
On Mon, Feb 26, 2007 at 04:35:06PM +0100, Pepe Iborra wrote:
I am really curious about this style of programming, and find myself playing with it from time to time. The example so far is very nice, but the funniest part is missing. That is, defining appendL.
appendL :: List a t1 -> List a t2 -> List a t3
This says that the append of a list of length t1 and a list of length t2 is a list of whatever length t3 we want. Obviously this is not true and will not typecheck. After some healthy days of reading papers and theses, I've found at least three ways of defining it.
First, via existentials:
appendL1 :: List a t1 -> List a t2 -> exists t3. List a t3
Second, attaching a proof. Question: what would be the advantage of the proof here?
data Add a b c where Base :: Add NilT a a ; Step :: Add a b c -> Add (ConsT a) b (ConsT c) appendL2 :: List a t1 -> List a t2 -> exists t3. (Add t1 t2 t3, List a t3)
Third, via Type Classes. \begin{code} class AddList a b c | a b -> c where append :: List x a -> List x b -> List x c instance AddList NilT b b where append Nil x = x instance AddList a b c => AddList (ConsT a) b (ConsT c) where append (Cons x l) l' = Cons x (append l l') \end{code}
Given the three methods, I wouldn't know which one should be preferred, and why. In the first one you pay the burden of programming with existentials. The second one in addition to that is the least efficient, as building the proof surely has a cost. Since we are building it, isn't there a way to use it to remove the existential? Finally, with the third one your compiler will produce error messages that will make you swear, apart from possible efficiency losses too.
Personally I like the GADT approach best since it is very flexible and convienient. I have never used a purpose-build computer proof system, but (modulo _|_) it took me less than 10 minutes to answer LoganCapaldo (on #haskell)'s challenge to proof that + was commutative ( http://hpaste.org/522 ). Now, efficiency concerns. GHC haskell already uses higher-than-value-level proofs to implement newtypes/GADTs/ATs; efficiency concerns are addressed in a strikingly adhoc way, by promoting equality to the KIND level, allowing type erasure to remove the overhead of checking. Chakravarty, Peyton Jones, we'd really like a general kind-level proof system!
participants (7)
-
apfelmus＠quantentunnel.de -
David Roundy -
Derek Elkins -
Matthew Brecknell -
Neil Mitchell -
Pepe Iborra -
Stefan O'Rear