Am Donnerstag, 31. Januar 2008 18:30 schrieb Dominic Steinitz:
Look at
This is essentially what I had in mind. While Oleg’s implementation needs a “thrusted core”, the GADT solution doesn’t. It would be interesting to combine GADTs with decimal type-level naturals. This could look like this:
class Succ val succ | val -> succ, succ -> val where
[…]
data List len elem where
Nil :: List Sz elem
Cons :: (Succ len len') => elem -> List len elem -> List len' elem
Or with efficient contcatenation:
class Sum val1 val2 sum | val1 val2 -> sum, val1 sum -> val2, val2 sum -> val1 where
[…]
data List len elem where
Empty :: List Sz elem
Singleton :: List (D1 Sz) elem
Append :: (Add len1 len2 len') => List len1 elem -> List len2 elem -> List len' elem
Note, that type families might make this code even nicer. Some words on the representation of decimal numbers as types. While the representation with types of the form D1 (D2 (D3 Sz)) has the advantage of allowing numbers of arbitrary size, it has the disadvantage of a growing number of parantheses. In my opinion, it would be nicer to have somethink like D1 :- D2 :- D9 :- () with a right-associative operator :-. We could even build the digit list the other way round—() :- D1 :- D2 :- D9—using a left-associative :-. With the latter representation, we wouldn’t need to reverse digit sequences when adding numbers. Well, the representation (D1,D2,D9) might be considered more readable. It has the disadvantage of a fixed maximum size for the numbers. Which takes me to a point I had already considered some time ago: Wouldn’t it be good if we had just a type data Pair val1 val2 = Pair val1 val2 and if then (val1,val2,…,valn) would just be syntactic sugar for this: val1 `Pair` (val2 `Pair` (…(valn `Pair` ())…)) Best wishes, Wolfgang