type-level integers using type families

[Peter Gavin]

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