TypeFamilies vs. FunctionalDependencies & type-level recursion
simonpj at microsoft.com
Fri Aug 5 15:50:45 CEST 2011
| > 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
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
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.
More information about the Haskell-prime