Future kind system, closed type functions and type classes

[Philip K.F. Hölzenspies]

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