I dont remember where i saw it, but i think someone had an example of a list whose type is the maximum element in the list. I've been trying to reproduce that with GADT's. data One = One data Two = Two data Three = Three data MaxList t where Elem1 :: MaxList One Elem2 :: MaxList Two ML1Cons1 :: MaxList One -> MaxList One -> MaxList One ML1Cons2 :: MaxList One -> MaxList Two -> MaxList Two ML2Cons1 :: MaxList Two -> MaxList One -> MaxList Two ML2Cons2 :: MaxList Two -> MaxList Two -> MaxList Two a = ML2Cons2 Elem2 $ ML2Cons1 Elem2 $ ML1Cons1 Elem1 $ Elem1 so one problem is the tedium of defining a cons for each possible combination. The other problem is that i cant define a usefull tail that makes any sense. mlTail :: MaxList Two -> MaxList t mlTail (ML2Cons2 a b) = b mlTail (ML2Cons1 a b) = b this one doesn't work, and probably because there is nothing that i could do with the return value. mlTail :: MaxList Two -> MaxList Two mlTail (ML2Cons2 a b) = b mlTail (ML2Cons1 a b) = b --wont compile because b is a MaxList One will only work for lists that only contain Two's, which is not what i want either. So is this somehow possible? Thanks
Anatoly Yakovenko
I dont remember where i saw it, but i think someone had an example of a list whose type is the maximum element in the list. I've been trying to reproduce that with GADT's.
data One = One data Two = Two data Three = Three
data MaxList t where Elem1 :: MaxList One Elem2 :: MaxList Two ML1Cons1 :: MaxList One -> MaxList One -> MaxList One ML1Cons2 :: MaxList One -> MaxList Two -> MaxList Two ML2Cons1 :: MaxList Two -> MaxList One -> MaxList Two ML2Cons2 :: MaxList Two -> MaxList Two -> MaxList Two
a = ML2Cons2 Elem2 $ ML2Cons1 Elem2 $ ML1Cons1 Elem1 $ Elem1
so one problem is the tedium of defining a cons for each possible combination. The other problem is that i cant define a usefull tail that makes any sense.
mlTail :: MaxList Two -> MaxList t mlTail (ML2Cons2 a b) = b mlTail (ML2Cons1 a b) = b
this one doesn't work, and probably because there is nothing that i could do with the return value.
Your problem in this example is that the t in "MaxList t" is universally quantified when it needs to be existentially quantified. The following definition encodes the existential quantification as a rank-2 type: mlTail :: MaxList n -> (forall t. MaxList t -> a) -> a mlTail (ML1Cons1 h t) f = f t mlTail (ML1Cons2 h t) f = f t mlTail (ML2Cons1 h t) f = f t mlTail (ML2Cons2 h t) f = f t It works with the rest of your code unmodified.
mlTail :: MaxList Two -> MaxList Two mlTail (ML2Cons2 a b) = b mlTail (ML2Cons1 a b) = b --wont compile because b is a MaxList One
will only work for lists that only contain Two's, which is not what i want either. So is this somehow possible?
This example here suggests that you are happy merely with a (not necessarily tight) upper bound on the list elements. The following code solves your problem in this case, using only type unification and not fundeps or TFs: data Nat a where Z :: Nat a S :: Nat a -> Nat (S a) data Z data S a n00 = Z n01 = S n00 n02 = S n01 n03 = S n02 n04 = S n03 data MaxList t where Nil :: MaxList a Cons :: Nat a -> MaxList a -> MaxList a a = Cons n02 $ Cons n02 $ Cons n01 $ Nil --- ":t a" gives "forall a. MaxList (S (S a))" which tells you exactly --- what you want: elements are at least 2. mlTail :: forall t. MaxList t -> MaxList t mlTail (Cons h t) = t --- unfortunately, you lose information here if the first --- element is larger than the rest. Reiner
data One = One data Two = Two data Three = Three
data MaxList t where Elem1 :: MaxList One Elem2 :: MaxList Two ML1Cons1 :: MaxList One -> MaxList One -> MaxList One ML1Cons2 :: MaxList One -> MaxList Two -> MaxList Two ML2Cons1 :: MaxList Two -> MaxList One -> MaxList Two ML2Cons2 :: MaxList Two -> MaxList Two -> MaxList Two
a = ML2Cons2 Elem2 $ ML2Cons1 Elem2 $ ML1Cons1 Elem1 $ Elem1
so one problem is the tedium of defining a cons for each possible combination. The other problem is that i cant define a usefull tail that makes any sense.
mlTail :: MaxList Two -> MaxList t mlTail (ML2Cons2 a b) = b mlTail (ML2Cons1 a b) = b
this one doesn't work, and probably because there is nothing that i could do with the return value.
Your problem in this example is that the t in "MaxList t" is universally quantified when it needs to be existentially quantified. The following definition encodes the existential quantification as a rank-2 type:
mlTail :: MaxList n -> (forall t. MaxList t -> a) -> a mlTail (ML1Cons1 h t) f = f t mlTail (ML1Cons2 h t) f = f t mlTail (ML2Cons1 h t) f = f t mlTail (ML2Cons2 h t) f = f t
It works with the rest of your code unmodified.
how do i define (forall t. MaxList t -> a)? It seems like i just pushed the problem somewhere else.
mlTail :: MaxList Two -> MaxList Two mlTail (ML2Cons2 a b) = b mlTail (ML2Cons1 a b) = b --wont compile because b is a MaxList One
will only work for lists that only contain Two's, which is not what i want either. So is this somehow possible?
This example here suggests that you are happy merely with a (not necessarily tight) upper bound on the list elements. The following code solves your problem in this case, using only type unification and not fundeps or TFs:
data Nat a where Z :: Nat a S :: Nat a -> Nat (S a)
data Z data S a
n00 = Z n01 = S n00 n02 = S n01 n03 = S n02 n04 = S n03
data MaxList t where Nil :: MaxList a Cons :: Nat a -> MaxList a -> MaxList a
a = Cons n02 $ Cons n02 $ Cons n01 $ Nil --- ":t a" gives "forall a. MaxList (S (S a))" which tells you exactly --- what you want: elements are at least 2.
mlTail :: forall t. MaxList t -> MaxList t mlTail (Cons h t) = t --- unfortunately, you lose information here if the first --- element is larger than the rest.
Thanks, that's really cool. Is there a way to keep a tight upper bound on the list using this method?
On Sat, Sep 20, 2008 at 1:12 PM, Anatoly Yakovenko
Your problem in this example is that the t in "MaxList t" is universally quantified when it needs to be existentially quantified. The following definition encodes the existential quantification as a rank-2 type:
mlTail :: MaxList n -> (forall t. MaxList t -> a) -> a mlTail (ML1Cons1 h t) f = f t mlTail (ML1Cons2 h t) f = f t mlTail (ML2Cons1 h t) f = f t mlTail (ML2Cons2 h t) f = f t
It works with the rest of your code unmodified.
how do i define (forall t. MaxList t -> a)? It seems like i just pushed the problem somewhere else.
Since MaxList is a GADT, you can always look inside to specialize the parameter. In fact, with this particular definition, you just have to look at the outermost constructor. findMax :: MaxList n -> Either (MaxList One) (MaxList Two) findMax l@Elem1 = Left l findMax l@Elem2 = Right l findMax l@(ML1Cons1 _ _) = Left l findMax l@(ML1Cons2 _ _) = Right l findMax l@(ML2Cons1 _ _) = Right l findMax l@(ML2Cons2 _ _) = Right l
This example here suggests that you are happy merely with a (not necessarily tight) upper bound on the list elements. The following code solves your problem in this case, using only type unification and not fundeps or TFs: [...] Thanks, that's really cool. Is there a way to keep a tight upper bound on the list using this method?
One way is to use a witnesses to prove that the head of the list is
either the maximum element, or less than (or equal) to the maximum
element.
data MaxList n where
Nil :: MaxList Z
ConsMax :: LE n a -> Nat a -> MaxList n -> MaxList a
ConsLE :: LE a n -> Nat a -> MaxList n -> MaxList n
cons :: Nat a -> MaxList b -> (forall n. MaxList n -> ans) -> ans
cons a as f = case cmp a (maximum as) of
Left le -> f (ConsLE le a as)
Right le -> f (ConsMax le a as)
mlTail :: MaxList a -> (forall b. MaxList b -> ans) -> ans
mlTail (ConsMax _ _ as) f = f as
mlTail (ConsLE _ _ as) f = f as
There are at least three ways to define LE, which have different
trade-offs in terms of usability and space efficiency. One way is to
encode both numbers,
data LE a b where
ZLE :: Nat b -> LE Z b
SLE :: LE a b -> LE (S a) (S b)
cmp :: Nat a -> Nat b -> Either (LE a b) (LE b a)
cmp Z b = Left (ZLE b)
cmp a Z = Right (ZLE a)
cmp (S a) (S b) = either (Left . SLE) (Right . SLE) (cmp a b)
maximum :: MaxList n -> Nat n
maximum Nil = Z
maximum (ConsMax _ n _) = n
maximum (ConsLE le _ _) = greater le
greater :: LE a b -> Nat b
greater (ZLE b) = b
greater (SLE l) = S (greater l)
lesser :: LE a b -> Nat a
lesser (ZLE b) = Z
lesser (SLE l) = S (lesser l)
Alternatively, you can encode the difference between a and b,
data LE a b where
Eq :: LE a a
Lt :: LE a b -> LE a (S b)
cmp :: Nat a -> Nat b -> Either (LE a b) (LE b a)
cmp Z Z = Left Eq
cmp Z (S b) = Left (Lt (zle b))
cmp (S a) Z = Right (Lt (zle a))
cmp (S a) (S b) = either (Left . sle) (Right . sle) (cmp a b)
zle :: Nat a -> LE Z a
zle Z = Eq
zle (S n) = Lt (zle n)
sle :: LE a b -> LE (S a) (S b)
sle Eq = Eq
sle (Lt l) = Lt (sle l)
-- Since only the types change, it should be safe to
-- replace sle with unsafeCoerce. In that case, the
-- final equation for cmp can just be
-- cmp (S a) (S b) = unsafeCoerce (cmp a b)
maximum :: MaxList n -> Nat n
maximum Nil = Z
maximum (ConsMax _ n _) = n
maximum (ConsLE le a _) = greater le a
greater :: LE a b -> Nat a -> Nat b
greater Eq n = n
greater (Lt l) n = S (greater l n)
lesser :: LE a b -> Nat b -> Nat a
lesser Eq n = n
lesser (Lt l) (S n) = lesser l n
--
Dave Menendez
Someone could probably give a better explanation but I'll give this a shot! :) What you are actually doing is defining a "family" of types. Every value in the type "Nat a" has it's own type. For instance "Z" has type "Nat Z", "(S Z)" or "one" has type "Nat (S Z)", "(S (S Z))" has type "Nat (S (S Z))" and so on. In effect types "Z" and "(S a)" defined in those data declarations are "marker" types. It might help you understand if you change the names of the types in the data declarations to something else. It helps not to get confused between types and constructors ;) . I hope this was helpful, Frank On 22 Sep 2008, at 21:42, Anatoly Yakovenko wrote:
data Nat a where Z :: Nat a S :: Nat a -> Nat (S a)
data Z data S a
I thought I was getting this, but this part is confusing. What exactly does declaring "data Z" do? _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On Mon, Sep 22, 2008 at 2:42 PM, Anatoly Yakovenko
data Nat a where Z :: Nat a S :: Nat a -> Nat (S a)
data Z data S a
I thought I was getting this, but this part is confusing. What exactly does declaring "data Z" do?
Well, in Haskell without closed type families, it's not doing all that much. You could use Int or IO Elephant if you wanted to, as long as its head is not S. But it's documentation, because we're really declaring the dependent type (in pseudohaskell): data Nat = Z | S Nat data Bounded :: Nat -> * where BZ :: Bounded n BS :: Bounded n -> Bounded (S n) So Z and S are the data constructors for Nat, and Bounded *should* only be able to take Nats as arguments. But we cannot express that in Haskell, we just have to be disciplined and never give anything else to Bounded. Luke
data Nat a where Z :: Nat a S :: Nat a -> Nat (S a)
data Z data S a
n00 = Z n01 = S n00 n02 = S n01 n03 = S n02 n04 = S n03
data MaxList t where Nil :: MaxList a Cons :: Nat a -> MaxList a -> MaxList a
a = Cons n02 $ Cons n02 $ Cons n01 $ Nil --- ":t a" gives "forall a. MaxList (S (S a))" which tells you exactly --- what you want: elements are at least 2.
mlTail :: forall t. MaxList t -> MaxList t mlTail (Cons h t) = t
Is there a way to define a function that only takes a list with a max of 1? Because only1 :: MaxList (S a) -> String only1 _ = "only1" will work over
a = Cons n02 $ Cons n02 $ Cons n01 $ Nil without any problems
On Mon, Sep 22, 2008 at 10:20 PM, Anatoly Yakovenko
Is there a way to define a function that only takes a list with a max of 1? Because
only1 :: MaxList (S a) -> String only1 _ = "only1"
will work over
a = Cons n02 $ Cons n02 $ Cons n01 $ Nil without any problems
only1 :: MaxList (S Z) -> String
If you like, you may declare
type One = S Z
type Two = S One
etc.
--
Dave Menendez
type One = S Z type Two = S One etc.
why does: data Nat a where Z :: Nat a S :: Nat a -> Nat (S a) data Z data S a type One = S Z n00 = Z n01::One = S n00 give me: test.hs:10:11: Couldn't match expected type `One' against inferred type `Nat (S a)' In the expression: S n00 In a pattern binding: n01 :: One = S n00 Failed, modules loaded: none. or better yet, how is type S Z different from, n01 :: forall a. Nat (S a)
Try
n01 :: Nat One
-- ryan
On Mon, Sep 22, 2008 at 8:10 PM, Anatoly Yakovenko
type One = S Z type Two = S One etc.
why does:
data Nat a where Z :: Nat a S :: Nat a -> Nat (S a)
data Z data S a
type One = S Z n00 = Z n01::One = S n00
give me:
test.hs:10:11: Couldn't match expected type `One' against inferred type `Nat (S a)' In the expression: S n00 In a pattern binding: n01 :: One = S n00 Failed, modules loaded: none.
or better yet, how is type S Z different from, n01 :: forall a. Nat (S a) _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
On Mon, Sep 22, 2008 at 11:10 PM, Anatoly Yakovenko
type One = S Z type Two = S One etc.
why does:
data Nat a where Z :: Nat a S :: Nat a -> Nat (S a)
data Z data S a
type One = S Z n00 = Z n01::One = S n00
give me:
test.hs:10:11: Couldn't match expected type `One' against inferred type `Nat (S a)' In the expression: S n00 In a pattern binding: n01 :: One = S n00 Failed, modules loaded: none.
or better yet, how is type S Z different from, n01 :: forall a. Nat (S a)
In short, S Z is a type and n01 is a value.
One point that's important to keep in mind is that types and data
constructors have disjoint namespaces, so you can have a type Z and a
data constructor Z which do not need to have any connection.
It may be clearer if we rename the data constructors for Nat.
data Z
data S n
type One = S Z
data Nat :: * -> * where
Zero :: Nat Z
Succ :: Nat n -> Nat (S n)
one :: Nat One
one = Succ Zero
Similarly, One is a type (One :: *) and one is a value (one :: Nat One
and Nat One :: *).
Note also that Z and S are declared here as empty types, using a
common extension. That means there are no (non-bottom) values that
have type Z or S a. This means that Z and S are only used as arguments
to other type constructors or in class contexts.
As long as we're discussing type-level naturals, you may find this old
post of mine interesting.
http://www.haskell.org/pipermail/haskell/2005-May/015815.html
--
Dave Menendez
has the "with" syntax described in
http://www.haskell.org/pipermail/haskell/2005-May/015815.html
been replaced with the "where" syntax? so data Foo a where FooInt :: FooInt the same thing as data Foo A = FooInt with a = Int
On Tue, Sep 30, 2008 at 6:25 PM, Anatoly Yakovenko
has the "with" syntax described in
http://www.haskell.org/pipermail/haskell/2005-May/015815.html
been replaced with the "where" syntax?
so
data Foo a where FooInt :: FooInt
the same thing as
data Foo A = FooInt with a = Int
I don't see any such syntax in the aforementioned message. But yes, the where syntax is currently the only way to do GADTs (and I hope that does *not* change, because I love the GADT syntax!): data Foo a where FooInt :: Foo Int Luke
participants (6)
-
Anatoly Yakovenko -
David Menendez -
Frank Wilson -
Luke Palmer -
Reiner Pope -
Ryan Ingram