writes:

Thanks David, For the +1 vote on the word "restraints". Yes, my thinking was that it was both sufficiently suggestive and sufficiently separate from "constraints". Also 'restrained' has an overtone of civilised and moderate, compared to the 'wild west' of overlaps and fundeps. I'm a bit hesitant to draw any conclusions from my comments, until I've seen something from the 'brains trust'. At least nobody's (yet) told me I'm being dumb. Yes, there could be many ways of encoding the type constructors, but that's not what I was worried about (nor about the context stack). Let me spell out the scenario: In my package/module, I declare some data types, and encode them with instances for TC_code. I import a library/module, which imports ..., which imports ... (Or my client combines my package into their project, with other imports.) That remote import declares different data types, but declares instances for TC_code whose RHS TypeRep are duplicates of mine. The only way (I can see) to be sure to avoid that is (as you suggest) encode the package, module and symbol. But GHC (and indeed Hugs) has a perfectly workable way to do that already. I don't know the internals of it, but I know it's good enough to drive overlapping instances *provided the types are grounded*. My view is that despite all the misgivings, overlaps have been remarkably successful and stable considering their poorly-understand theoretical basis, and lack of any real work on them for going on a decade. (The HList paper is 2004, there's since been all sorts of fancy type innovations, including families, but all of the HList stuff still works.) There is more subtlety in Oleg's proposal than I at first understood. He does indeed ground all the types by applying constructors to the unit type (), when passing to TYPEOF. So Oleg's correct to say "The arguments to StateT ... are irrelevant ..." (Combined with all the parentheses for the type-level Succ's, his code is beginning to look suspiciously LISP-like ;-) But unground types were a concern with HList, where you're trying to simulate extensible records, and combining data with Higher-level functions a la Object- oriented style. Another (possible) example of ungroundedness is the IsFunction type function:

instance IsFunction (a -> b) = TTrue -- a, b not grounded instance IsFunction a | a /~ (_ -> _) = TFalse -- deliberately use `_` placeholder for the args, -- because it's meaningless to ground them

For type inference to work there, we don't need to refine the type beyond its outermost type constructor. (And this is one example where currently HList's TypeEq doesn't always work for polymorphic functions.) As another example of Oleg's subtleties, I hadn't realised that you could include more than one type constructor for your 'Special instances': Type Special is a list (HList-like), not a single type. (Again with each element having the constructor grounded on () arguments.) But the Special instances have to be declared all together. So I don't see this as providing any greater flexibility than Closed type classes, or a finite number of instances declared with inequality restraints. AntC

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