Hi Wolfgang,
On Feb 10, 2008 5:43 PM, Wolfgang Jeltsch
(<+>) :: 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