Dear all, My apologies for the lengthy mail. There is a question at the end about whether all types in (of?) a kind closed under a type function can be concluded to be a member of a type class (i.e. whether kind classes are required for what I want to do). I have been trying to reserect Robert Dockins' TypeNats library [1], by pulling it out of the type classes / functional dependencies space and into the type family space. The current (discontinued) TypeNats has one Very Nice Thing to it; naturals are coded as bits, rather than as plain successors. Length annotations of vectors et al. now have a memory complexity of O(lg N) as opposed to O(N). A naïve implementation attempt runs into a rather obvious problem: data Z data I n data O n class Natural n where type Pred n toIntegral :: Integral i => n -> i toPred :: Natural n => n -> Pred n toPred _ = undefined instance Natural Z where type Pred Z = Z toIntegral _ = 0 instance Natural (I n) where type Pred (I n) = O n toIntegral n = let i = toIntegral (toPred n) in succ (i+i) instance Natural (O n) where type Pred (O n) = I (Pred n) toIntegral n = let i = toIntegral (toPred n) in i+i This should be interpreted as follows: Z denotes the empty bit string. I denotes a 1 and O denotes a 0. The bits are in reversed order, so 6 is coded as O(I(I Z)). One would expect the instance declaration of O to require a context "Natural n," because of "Pred n" and "toPred n," but the type checker allows for this. As a matter of fact, introducing the context "Natural n" to both the instance declarations of I and O raises the error: Could not deduce (Natural (Pred n)) from the context (Integral a) arising from a use of `natToIntegral' (in the instance declaration of O n) Leaving the context out, this implementation causes stack overflows when evaluating "toIntegral (undefined :: I Z)", because (O Z) is not reduced to Z. The FD solution is to introduce a class that describes the "canonical form" of a bit string (where the canonical form of O Z is Z): class Canonical n cfunctions for Haskell Tom Schrijv | n -> c Since we now have type functions, we can express this in a considerably more comprehensive manner. We can simply write: type family CanonicalNat c type family CanonicalNat_ c type instance CanonicalNat Z = Z type instance CanonicalNat (I n) = I (CanonicalNat n) type instance CanonicalNat (O n) = CanonicalNat_ (O (CanonicalNat n)) type instance CanonicalNat_ (O Z) = Z type instance CanonicalNat_ (O (O n)) = O (O n) type instance CanonicalNat_ (O (I n)) = O (I n) With the type function CanonicalNat, toPred can now be redefined to give a predecessor of a canonical type: toPred :: Natural n => n -> CanonicalNat (Pred n) toPred _ = undefined Unfortunately: Could not deduce (Natural (CanonicalNat_ (O (CanonicalNat n)))) from the context (Integral a) arising from a use of `natToIntegral' Adding a context to the definitions of I and O, viz. data Natural n => I n data Natural n => O n doesn't help very much. I'm no inference expert, but it seems that the problem is that inference goes up, not down (or vice versa, depending on how you interpret these words). Also, adding contexts to the results of type functions is a non-trivial thing [2]). In Schrijvers et al. [3], it is mentioned that work is being undertaken in the direction of closed type functions by using kind declarations. For this example, this would look something like: datakind NatNum = Z | I NatNum | O NatNum and type family CanonicalNat (c :: NatNum) :: NatNum Ideas for a new kind system for GHC is discussed on the wiki [4]. The interaction with type classes section shows this example (for Z/Succ represented Peano numbers): data kind Nat = Zero | Succ Nat class LessThanOrEqual (n1 :: Nat) (n2 :: Nat) instance LessThanOrEqual Zero Zero instance LessThanOrEqual n m => LessThanOrEqual n (Succ m) Aside from the fact that I would imagine that there is a missing case here instance LessThanOrEqual n m => LessThanOrEqual (Succ n) (Succ m) which is non-trivial because of the overlap with the second instance declaration, it is hard for me to see whether a checker with this new kind system could decide that all types in Nat have corresponding instances in LessThanOrEqual. It should be clear how this relates to my case described above; can it now be decided that the result of CanonicalNat will always have an instance of the Natural class? Regards, Philip PS. A possible purpose of a function such as toIntegral is to have a length implementation for fixed-length lists that is more lazy than the length function on a list, but that can be used in exactly the same way. [1] http://www.cs.princeton.edu/~rdockins/dist/typenats-0.2-source.tar.gz [2] http://content.ohsu.edu/cgi-bin/showfile.exe?CISOROOT=/etd&CISOPTR=227&filename=7031321462007_200705.diatchki.iavor.pdf [3] http://research.microsoft.com/~simonpj/papers/assoc-types/ifl2007.pdf [4] http://hackage.haskell.org/trac/ghc/wiki/KindSystem