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

[Alfonso Acosta]

Hi Wolfgang,


On Feb 10, 2008 5:43 PM, Wolfgang Jeltsch <g9ks157k at acme.softbase.org> wrote:

I added some line annotations to the code below so that errors can be
more easily understood

> > (<+>) :: Add s1 s2 s3 => FSVec s1 a -> FSVec s2 a -> FSVec s3 a -- line 78
> > NullV  <+> ys  = ys -- line 79
> > (x:>xs) <+> ys = x :> (xs <+> ys) -- line 80
>
> Hmm, we would have to find a way to implement lemmas.  In this case, the lemma
> that succ (x + y) = succ x + y.  At the moment, I've no good idea how to do
> that.

I'm not sure if that is the only problem.

I already mentioned I'm a noob with GADTs so I might be wrong but it
seems that emulating dependent types with multiparameter type classes
or type synonym families (more on this below) and GADT pattern
matching does not work nicely.  In the case of <+>, three errors are
generated:

1)
    Couldn't match expected type `s3' against inferred type `s2'
      `s3' is a rigid type variable bound by
           the type signature for `<+>' at Data/Param/FSVec.hs:78:19
      `s2' is a rigid type variable bound by
           the type signature for `<+>' at Data/Param/FSVec.hs:78:16
      Expected type: FSVec s3 a
      Inferred type: FSVec s2 a

2)
    Could not deduce (Data.TypeLevel.Num.Sets.PosI s3,
                      Data.TypeLevel.Num.Ops.NClassify s3 yc,
                      Data.TypeLevel.Num.Ops.DivMod10 yh yl s3)
      from the context (Succ s11 s1)

3)
    Could not deduce (Data.TypeLevel.Num.Ops.Add' s11 s2 s,
                      Data.TypeLevel.Num.Ops.Add' s2 s11 s)
      from the context (Succ s11 s1)
      arising from a use of `<+>'


So defining the lema you mentioned (succ (x + y) = succ x + y)
wouldn't solve the whole problem. Actually (2) wouldn't happen if the
context of the function was taken into account (i.e.  "from the
context (Succ s11 s1)" should be "from the context (Succ s11 s1, Add
s1 s2 s3)". Can someone explain why GHC does not behave like that?


I don't know if type synonym families would help for <+> but certainly
they don't for tailV:


> > tailV :: Succ s' s => FSVec s a -> FSVec s' a
> > tailV (x :> xs) = xs
>
> Maybe this problem is similar to the one I came across earlier.  See my mail
> on <http://www.haskell.org/pipermail/haskell/2007-September/019757.html> and
> the replies to it.


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.

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


My first impressions about using type synonym families (as opposed to
multiparameter type classes) to fake dependent types are:

* Positive part:
  - Operations on types can really be expressed as functions on types
which is more natural than using MTPC-constraints. Infox operands are
particularly expressive. For example:

-- Add type family
type family (:+:) x y :: *

 - According to
http://www.haskell.org/pipermail/haskell/2007-September/019759.html
They fit in a nicer way with the Haskell standard.

* Negative part:

  - They don't allow defining relational type operations, which is
_really_ important to dramatically reduce the number of necessary
instances.
 i.e Pred cannot be defined out of Succ, this declaration is ilegal

type family Pred x :: *
type instance Pred (Succ x) =  x

whereas it is perfecty possible using MTPCs

class (Pos x, Nat y) => Pred x y | x -> y, y -> x
instance Succ x y => Pred y x


 - 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

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 !

----
Conclusion
----

So, it seems that with or without type synonym families GADTs don't
work so nicely to emulate dependent types (or at least
numer-parameterized data structures), so I'll move on to traditional
phantom types unless someone provides a solution.

I'd like to be proven wrong (we'll lose pattern matching without GADTs
which is a pity) but I cannot come up with a better solution.

On the other hand, using phantom type parameters allows to encapsulate
whichever vector representation we want "under the hood".

And that's actually the approach followed by Fredrik Eaton's Vectro
library: http://ofb.net/~frederik/vectro/

So unless someone provides a solution for the GADT problem, I think
the best option would be simply adapting Vectro to work with the
type-level library.



> > The result would be a function with the following type:
> >
> > vector :: [a] -> (forall s . Nat s => FSVec s a -> w) -> w
> >
> > Nevertheless, I'm not fully satisfied by it.
>
> I suppose, it's the best we can get without having dependent types.  Others
> might correct me.

Well, if that's all it can be done (and that's what it seems from your
answers), satisfied or not, there's no better option.


>
> 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 ...)

Best Regards,

A really frustrated Fons

PS:

Implemnetaion of Succ using a type synonym family.

-- | Successor type-level relation
type family Succ x :: *

type instance Succ D0 = D1
type instance Succ D1 = D2
type instance Succ D2 = D3
type instance Succ D3 = D4
type instance Succ D4 = D5
type instance Succ D5 = D6
type instance Succ D6 = D7
type instance Succ D7 = D8
type instance Succ D9 = (D1 :* D0)
type instance Succ (x :* D0) = x :* D1
type instance Succ (x :* D1) = x :* D2
type instance Succ (x :* D2) = x :* D3
type instance Succ (x :* D3) = x :* D4
type instance Succ (x :* D4) = x :* D5
type instance Succ (x :* D5) = x :* D6
type instance Succ (x :* D6) = x :* D7
type instance Succ (x :* D7) = x :* D8
type instance Succ (x :* D8) = x :* D9
type instance Succ (x :* D9) = (Succ x) :* D0

-- | value-level reflection function for the succesor type-level relation
--   (named succRef to avoid a clash with 'Prelude.succ')
succRef :: Nat x => x -> Succ x
succRef = undefined