type-level integers using type families
Peter Gavin
pgavin at gmail.com
Sat May 31 11:47:13 EDT 2008
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
More information about the Libraries
mailing list