[Haskell-cafe] [ghc-proposals/cafe] Partially applied type families
anthony_clayden at clear.net.nz
Sun Jun 4 08:06:32 UTC 2017
> 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
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
* 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
Then we can use the instance mechanism to extend
("Usual" for example with DSL's to expand the AST.)
If you have closed type families/classes (esp in an
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
Garrett in an earlier message quoted section 3.1.1 of the
"a class can be populated by multiple, non-overlapping
instance chains, where each chain may contain multiple
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
> 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
Another style of carrying the payload is type labels.
To mix these styles, I need a way to cons a labelled
> 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
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
but provide a mechanism to enforce no-overlaps.
And I think guards achieve that with relatively lightweight
avoiding hard-to-follow sequences of `else` ...
More information about the Haskell-Cafe