TypeFamilies vs. FunctionalDependencies & type-level recursion

[Simon Peyton-Jones]

Oleg

| > There seems no reason in principle to disallow
| > 	type instance F where
| > 	  F Int = Bool
| > 	  F a = [a]
| 
| 
| I would implement this as follows:
| 
| > type instance F x = F' (EQ (TYPEOF x) INT) x
| > type family F' trep x
| > type instance F' TRUE  x = Bool
| > type instance F' FALSE x = [x]

But you have just pushed the problem off to the definition of EQ.  And your definition of EQ requires a finite enumeration of all types, I think.  But * is open, so that's hard to do. What you want is
   type instance EQ where
       EQ a a = TRUE
       EQ _ _ = FALSE
and now we are back where we started.

Moreover, encoding the negative conditions that turn an arbitrary collection of equations with a top-to-bottom reading into a set of independent equations, is pretty tedious.

| First of all, can something be done about the behavior reported by
| David and discussed in the first part of the message
| 
|    http://www.haskell.org/pipermail/haskell-prime/2011-July/003489.html

OK.  Can you give a small standalone test case to demonstrate the problem, and open a Track ticket for it?

| Second, what is the status of Nat kinds and other type-level data that
| Conor was/is working on? 

Julien is working hard on an implementation right now.  The Wiki page is here
	http://hackage.haskell.org/trac/ghc/wiki/GhcKinds
Attached there are documents describing what we are up to.

| Would it be possible to add TYPEREP (type-level type representation)
| as a kind, similar to that of natural numbers and booleans?

Yes!  See 5.4 of "the theory document". It's still very incoherent, but it's coming along.

Simon