TypeFamilies vs. FunctionalDependencies & typelevel recursion
Simon PeytonJones
simonpj at microsoft.com
Fri Aug 5 15:50:45 CEST 2011
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 toptobottom 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/haskellprime/2011July/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 typelevel 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 (typelevel 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
More information about the Haskellprime
mailing list