[Haskell-cafe] Re: type-level integers using type families
On Thu, May 29, 2008 at 5:15 AM, Peter Gavin [EMAIL PROTECTED] wrote: Has anyone else tried implementing type-level integers using type families? When I started to work on thetype-level and parameterized data packages, I considered using type-families and GADTs, but I found quite a few problems which have been nicely summarized by Benedikt in this thread. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: type-level integers using type families
Benedikt Huber wrote: data True data False type family Cond x y z type instance Cond True y z = y type instance Cond False y z = z I'm not sure if this is what you had in mind, but I also found that e.g. type instance Mod x y = Cond (y :: x) x (Mod (Sub x y) y) won't terminate, as Mod D0 D1 == Cond True D0 (Mod (Sub D0 D1) D0) == loop Right, because it always tries to infer the (Mod (Sub x y) y) part no matter what the result of (y :: x) is. rather than Mod D0 D1 == Cond True D0 ? == D0 For Mod, I used the following (usual) encoding: type family Mod' x y x_gt_y type instance Mod' x y False = x type instance Mod' x y True = Mod' (Sub x y) y ((Sub x y) :=: y) type family Mod x y type instance Mod x y = Mod' x y (x :=: y) Yes, it's possible to terminate a loop by matching the type argument directly. 1) One cannot define type equality (unless total type families become available), i.e. use the overlapping instances trick: instance Eq e e True instance Eq e e' False I didn't want to mix type classes and families in my implementation. All the predicates are implemented like so: type family Eq x y type instance Eq D0 D0 = True type instance Eq D1 D1 = True ... type instance Eq (xh :* xl) (yh :* yl) = And (Eq xl yl) (Eq xh yh) then I've added a single type-class class Require b instance Require True so you can do stuff like f :: (Require (Eq (x :+: y) z)) = x - y - z or whatever. I haven't yet tested it (but I think it should work) :) Pete Consequently, all type-level functions which depend on type equality (see HList) need to be encoded using type classes. 2) One cannot use superclass contexts to derive instances e.g. to define instance Succ (s,s') = Pred (s',s) In constrast, when using MPTC + FD, one can establish more than one TL function in one definition class Succ x x' | x - x', x' - x 3) Not sure if this is a problem in general, but I think you cannot restrict the set of type family instances easily. E.g., if you have an instance type instance Mod10 (x :* D0) = D0 then you also have Mod10 (FooBar :* D0) ~ D0 What would be nice is something like type instance (IsPos x) = Mod10 (x :* D0) = D0 though type family AssertThen b x type instance AssertThen True x = x type instance Mod10 (x :* D0) = AssertThen (IsPos x) D0 seems to work as well. 4) Not really a limitation, but if you want to use instance methods of Nat or Bool (e.g. toBool) on the callee site, you have to provide context that the type level functions are closed w.r.t. to the type class: test_1a :: forall a b b1 b2 b3. (b1 ~ And a b, b2 ~ Not (Or a b), b3 ~ Or b1 b2, Bool b3) = a - b - Prelude.Bool test_1a a b = toBool (undefined :: b3) Actually, I think the 'a ~ b' syntax is very nice. I'm really looking forward to type families. best regards, benedikt ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: type-level integers using type families
Replying to myself... I put a copy of the darcs repo at http://code.haskell.org/~pgavin/tfp, if anyone is interested. Pete Peter Gavin wrote: Has anyone else tried implementing type-level integers using type families? I tried using a couple of other type level arithmetic libraries (including type-level on Hackage) and they felt a bit clumsy to use. I started looking at type families and realized I could pretty much build an entire Scheme-like language based on them. In short, I've got addition, subtraction, multiplication working after just a days worth of hacking. I'm going to post the darcs archive sometime, sooner if anyone's interested. I really like the type-families based approach to this, it's a lot easier to understand, and you can think about things functionally instead of relationally. (Switching back and forth between Prolog-ish thinking and Haskell gets old quick.) Plus you can do type arithmetic directly in place, instead of using type classes everywhere. One thing that I'd like to be able to do is lazy unification on type instances, so that things like data True data False type family Cond x y z type instance Cond True y z = y type instance Cond False y z = z will work if the non-taken branch can't be unified with anything. Is this planned? Is it even feasible? I'm pretty sure it would be possible to implement a Lambda like this, but I'm not seeing it yet. Any ideas? Pete ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: type-level integers using type families
Peter Gavin schrieb:
Has anyone else tried implementing type-level integers using type families?
I tried using a couple of other type level arithmetic libraries
(including type-level on Hackage) and they felt a bit clumsy to use. I
started looking at type families and realized I could pretty much build
an entire Scheme-like language based on them.
In short, I've got addition, subtraction, multiplication working after
just a days worth of hacking. I'm going to post the darcs archive
sometime, sooner if anyone's interested.
I really like the type-families based approach to this, it's a lot
easier to understand, and you can think about things functionally
instead of relationally. (Switching back and forth between Prolog-ish
thinking and Haskell gets old quick.) Plus you can do type arithmetic
directly in place, instead of using type classes everywhere.
I tried to rewrite Alfonso Acosta's type-level library (the one on
hackage) using type-families too, because, right, they are much nicer to
use than MPTCs.
It is a straigtforward translation, I've uploaded it to
http://code.haskell.org/~bhuber/type-level-tf-0.2.1.tar.gz
now (relevant files: src/Data/TypeLevel/{Bool.hs,Num/Ops.hs}).
I've also added a type-level ackermann to torture ghc a little bit ;),
but left out logarithms. Plus, I did very little testing.
One thing that I'd like to be able to do is lazy unification on type instances,
so that things like
data True
data False
type family Cond x y z
type instance Cond True y z = y
type instance Cond False y z = z
I'm not sure if this is what you had in mind, but I also found that e.g.
type instance Mod x y = Cond (y :: x) x (Mod (Sub x y) y)
won't terminate, as
Mod D0 D1 == Cond True D0 (Mod (Sub D0 D1) D0) == loop
rather than
Mod D0 D1 == Cond True D0 ? == D0
For Mod, I used the following (usual) encoding:
type family Mod' x y x_gt_y
type instance Mod' x y False = x
type instance Mod' x y True = Mod' (Sub x y) y ((Sub x y) :=: y)
type family Mod x y
type instance Mod x y = Mod' x y (x :=: y)
There are few other things you cannot do with type families, and some
for which you need type classes anyway (Alfonso pointed me to
http://www.haskell.org/pipermail/haskell-cafe/2008-February/039489.html
). Here's what I found:
1) One cannot define type equality (unless total type families become
available), i.e. use the overlapping instances trick:
instance Eq e e True
instance Eq e e' False
Consequently, all type-level functions which depend on type equality
(see HList) need to be encoded using type classes.
2) One cannot use superclass contexts to derive instances e.g. to define
instance Succ (s,s') = Pred (s',s)
In constrast, when using MPTC + FD, one can establish more than one TL
function in one definition
class Succ x x' | x - x', x' - x
3) Not sure if this is a problem in general, but I think you cannot
restrict the set of type family instances easily.
E.g., if you have an instance
type instance Mod10 (x :* D0) = D0
then you also have
Mod10 (FooBar :* D0) ~ D0
What would be nice is something like
type instance (IsPos x) = Mod10 (x :* D0) = D0
though
type family AssertThen b x
type instance AssertThen True x = x
type instance Mod10 (x :* D0) = AssertThen (IsPos x) D0
seems to work as well.
4) Not really a limitation, but if you want to use instance methods of
Nat or Bool (e.g. toBool) on the callee site, you have to provide
context that the type level functions are closed w.r.t. to the type class:
test_1a :: forall a b b1 b2 b3.
(b1 ~ And a b,
b2 ~ Not (Or a b),
b3 ~ Or b1 b2,
Bool b3) = a - b - Prelude.Bool
test_1a a b = toBool (undefined :: b3)
Actually, I think the 'a ~ b' syntax is very nice.
I'm really looking forward to type families.
best regards,
benedikt
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
