[Haskell-cafe] Re: Implementing fixed-sized vectors (using
g9ks157k at acme.softbase.org
Mon Feb 11 14:14:30 EST 2008
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
> > 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
More information about the Haskell-Cafe