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
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
