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