[Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)

[Wolfgang Jeltsch]

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

> […]