On Fri Jun 2 13:20:13 UTC 2017, Richard Eisenberg wrote:
On Jun 2, 2017, at 3:22 AM, Anthony Clayden wrote:
I hereby pronounce
instance TypeError ... => C Int Bool
as "not an instance". ...
Hmm. I'd be interested how you're going to stop the compiler matching some usage site to it.
That's what TypeError does. When the compiler matches a use site, it issues an error. I would imagine that's the behavior you want.
No. I want to leave the class open, so I can add other instances (possibly in a different module). If I protect instances in this module with guards, the compiler can satisfy itself that the other modules' instances do not overlap.
Can you write a concrete example of something you'd like to do that the current machinery doesn't?
OK let's recap the Expression Problem first. There are two legs: * We want to freely add methods over a set of datatypes. (Problematic in OOP, because the methods are embedded in the objects.) In Haskell we can declare a new class with new method(s), and give instances over those datatypes. * We want to freely add constructors, and expand existing classes/methods to cover. That's not so easy in Haskell. The usual work-round is to make each constructor a new datatype. Then we can use the instance mechanism to extend classes/methods. ("Usual" for example with DSL's to expand the AST.) If you have closed type families/classes (esp in an imported/library module), you're blocked from extending it for new datatypes. Now apparently Instance Chains don't suffer this, the `fails` triggers a search for other instances in other chains. Garrett in an earlier message quoted section 3.1.1 of the paper "a class can be populated by multiple, non-overlapping instance chains, where each chain may contain multiple clauses". Unfortunately I can find no examples of using this feature, so I'm a bit unsure how it goes. We'd know the chains are non-overlapping because they'd chain over distinct datatypes, I imagine. And I thought that's what we were getting with CTFs, but the implementation fell short of my expectations. I wanted (when I suggested the `where`-style syntax):
module A type family F a b -- full stop! type instance F (T1 a) b where ... -- overlapping equations within T1
module B type instance F (T2 c) d where ... -- overlapping equations within T2
Those closed instances in distinct modules are provably non-overlapping, because of the different type constructor. (By the same rules as currently, for apartness of instance heads. All equations within the where-group must unify with the instance head.) So then this (current) syntax would be a shorthand:
type family G e f where ... -- total equations for G
for the author of `G` who deliberately wanted to prevent anybody expanding the family. i.e shorthand for
type family G e f type instance G e f where ...
Fair enough, that's a common requirement. But all we got in the implementation was that blitz-all style. (I'm grumpy.) And according to Garrett's survey, 15% of Hackage would be grumpy too. OK, concrete example: within the HList framework
data HNil = HNil data HList e l = HList e l -- deliberately not using DataKinds
the Hlist paper discusses various approaches for indexing the payloads `e` within the list. Suppose (eliding a lot of detail) I choose Type-Indexed Products like
newtype PersonId = PersonId Int newtype PersonName = PersonName String ... me = HCons (PersonId 41) $ HCons (PersonName "AntC") HNil
And type indexed `Has` predicate needing overlaps:
class Has e l ... -- no instance for HNil instance Has e (HCons e l) ... instance (Has e l') => Has e (HCons e' l') ...
That's standard HList TIP, let's assume it's in a library/module. Another style of carrying the payload is type labels. To mix these styles, I need a way to cons a labelled element:
data AstroSign = AstroSign ... data HConsLab lab e l = HConsLab lab e l
me2 = HConsLab AstroSign 12 me
This deliberately allows the payload to be an ad-hoc type. Now I need a Has instance:
instance Has lab (HConsLab lab e l) ... instance (Has lab l') => Has lab (HConsLab lab' e' l') ...
Again relies on overlap. No danger of clashing with the vanilla HCons style, because labels are a distinct set of types. IOW this is fine:
you = HCons (PersonId 73) $ HCons (PersonName "rae") $ HConsLab AstroSIgn 7 HNil -- instances for the type of `you` -- (Has you PersonId, Has you PersonName, Has you AstroSign)
I can do all this now with stand-alone instances. But I have to be careful to keep my overlaps well-behaved. With closed Type Families/the proposed Classes, I can't add those HConsLab instances. I want to continue current support for freely adding instances, but provide a mechanism to enforce no-overlaps. And I think guards achieve that with relatively lightweight syntax, avoiding hard-to-follow sequences of `else` ... AntC