Am Montag, 11. Februar 2008 18:17 schrieben Sie:
[…]
As suggested by the pointer you provided, I redefined FSVec and tailV using a transformating of Succ into a type synonym family (see the end of this mail for its full definition) but it didn't help.
Be careful! Type family support is still broken in GHC 6.8. And the whole type system machinery seemed to be rather broken when I last checked a then current development version (6.9).
data FSVec :: * -> * -> * where NullV :: FSVec D0 a (:>) :: FSVec s a -> FSVec (Succ s) a
tailV :: FSVec s a -> FSVec (Succ s) a tailV (x :> xs) = xs
tailV leads to this error (which I don't really understand :S)
GADT pattern match in non-rigid context for `:>' Tell GHC HQ if you'd like this to unify the context In the pattern: x :> xs In the definition of `tailV': tailV (x :> xs) = xs
I think, this can be solved with a type declaration. At least I heard about something like this. Probably googling for this error message will help.
My first impressions about using type synonym families (as opposed to multiparameter type classes) to fake dependent types are:
[…]
I think, type synonym families are not a replacement for multiparameter classes but for functional dependencies. So you will still need multiparameter classes in certain places but you’ll be able to get rid of functional dependencies (except for certain cases where fundeps are combined with overlapping instances, at least).
- I'm maybe missing something, but it seems that type synonym families don't work nicely with typeclass constraints.
this is ilegal (syntax error):
type family Nat x => Succ x :: *
this is ilegal too (another syntax error):
type instance Nat x => Succ (x :* D0) = x :* D1
Maybe you should put your type family synonym into a class where it becomes an associated type synonym: class Nat x where type Succ x :: * […]
and finally I was really surprised to know that, using the type synonym family this is illegal too!
toInt (succRef d0)
the expression above leads to the following error:
No instance for (Data.TypeLevel.Num.Sets.NatI (Succ D0))
But .... Succ D0 = D1, and D1 and D1 _is_ an instance of NatI !
Maybe a bug. As I said, you cannot expect type families to work reliably at the moment.
[…]
Some remark concerning spelling: Would it be possible to drop the V at the end of the function names? I think the fact that those functions are about "vectors" is better expressed by qualification:
Right, do you think the same should be done for Data.TypeLeve.Num.Ops ? (succRef, predRef, addRef, subRef and friends ...)
Yes, I think so.
Best Regards,
A really frustrated Fons
:-( Best wishes, Wolfgang
[…]