At Sun, 26 Jun 2011 23:25:31 +1200, Anthony Clayden wrote:
Totally brilliant, and almost impenetrable.
If I understand what's going on (big IF), I'm wondering a few things: - You've used type-level NAT to encode the type. What if two different types get encoded as the same NAT? In your MonadState example you've encoded StateT as FOUR ::: NAT, and W as FIVE. What if there's some other module (in a distant import) that also uses FOUR? In general, how do we co-ordinate the encoding of types to avoid duplicates?
I think the type-level Nats are just an example. Another way to encode it would be in binary: data Z data Bit0 a data Bit1 a type family NatEq x y :: * type instance NatEq Z Z = HTrue type instance NatEq (Bit0 a) Z = HFalse type instance NatEq (Bit1 a) Z = HFalse type instance NatEq Z (Bit0 a) = HFalse type instance NatEq Z (Bit1 a) = HFalse type instance NatEq (Bit0 a) (Bit1 b) = HFalse type instance NatEq (Bit0 a) (Bit0 b) = NatEq a b type instance NatEq (Bit1 a) (Bit1 b) = NatEq a b Then you could encode the package, module, and symbol name as a type. Except even without UndecidableInstances you'll still easily blow through GHC's default context stack depth of 21, so that needs to be increased...
- Groundedness issues (per Section 9 of the HList paper, 'Reification ...' subsection. The instances of TYPEOF require the type constructor to be grounded; and TYPEOF recurses to reify all the constructor's type arguments. Does this mean all types and arguments have to be fully grounded?
Oleg's TYPEOF type function returns both a code for the constructor, and a list of types of the arguments. I think the idea is that both are ground types even if the type arguments they represent are not.
Is this really gaining anything over the Type-indexed rows approach you discuss in the HList paper - that is, using instances instance TypeEq x x HTrue instance (b ~ HFalse) => TypeEq x y b -- (using ~ instead of TypeCast) except that it's avoiding fundeps and overlapping instances? That is: is the TYPEOF approach to type equality going to suffer the same issues discussed at the start of section 9 'By chance or by design'?
It is essentially a translation of section 9 from fundeps to type families, so I would imagine the same limitations apply. However, I'm wondering where this is really a problem. I mean the kind of TYPEOF is * -> *, so you have to feed it a ground type anyway. Are there situations where you want to decide equality of non-ground types, and you can't just translate them to ground types through appropriate functions returning undefined? E.g., if you have something of type m a and m' b and want to know if m ~? m', just run both values through: toUnit :: m a -> m () toUnit _ = undefined
I'm imagining a Haskell' with type functions and a restrained sort of instance overlap: type instance TypeEqF x x = HTrue type instance TypeEqF x y | x /~ y = HFalse
(Which is roughly what last month's Haskell-prime discussion talked about, and SPJ picked up on at the start of this TypeFamilies thread.)
Yes, this is obviously something I would like. It is a far more drastic change to the language than what Oleg is suggesting. All Oleg needs is auto-derived instances, which could be done by a pre-processor with no modifications to the core compiler. However, in most cases such an inequality "restraint" (it's good not to call it a constraint, as constraints are typically not consulted for instance selection) would specify what programmers want more directly and likely lead to more readable code. David