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
