GHC: Ticket #9840: Permit empty closed type families
http://ghc.haskell.org/trac/ghc/ticket/9840
<p>
At the moment, closed type families without any equations fail with a parse error. In addition, they cannot be created by TH (see <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/8028" title="#8028: bug: Panic on degenerate closed type family (closed: fixed)">#8028</a>). Would it be possible to permit these instead?
</p>
<p>
My use case is in my typechecker plugin for units of measure, where I want to add new type-level operators without any equational theory (because it will be supplied by the plugin) and without users having the ability to introduce their own type family instances.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/9840
Trac 1.2.2simonpjThu, 27 Nov 2014 14:26:22 GMT
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:1
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:1
<p>
But you also want them to be non injective? Otherwise you could say
</p>
<pre class="wiki">data Plus a b
</pre><p>
Yes, feel free to offer a patch. Don't forget the user manual.
</p>
TicketgoldfireFri, 28 Nov 2014 03:28:43 GMT
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:2
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:2
<p>
I'm in support of this, too. But I won't have time to implement before the feature freeze...
</p>
TicketadamgundryWed, 15 Apr 2015 09:25:10 GMTstatus changed; differential, related set
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:3
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:3
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>patch</em>
</li>
<li><strong>differential</strong>
set to <em>Phab:D841</em>
</li>
<li><strong>related</strong>
set to <em>#8028</em>
</li>
</ul>
TicketgoldfireFri, 17 Apr 2015 12:52:48 GMT
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:4
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:4
<p>
I'm afraid something smells a little off here.
</p>
<p>
I agree that we should permit empty closed type families -- that's not a problem. But I'm not convinced that empty CTFs are the solution to Adam's problem.
</p>
<p>
What Adam really wants here is the ability to create new type-level constants at arbitrary kind. An empty CTF fits the bill, but there's something strange about it. Despite my early objections, I've come to agree with Lennart's viewpoint in <a class="new ticket" href="http://ghc.haskell.org/trac/ghc/ticket/9636" title="#9636: bug: Function with type error accepted (new)">#9636</a> that a CTF that is known to be unable to reduce is a strange beast that should probably be disallowed.
</p>
<p>
Here is a simple proposal:
</p>
<pre class="wiki">type constant Unit :: *
-- kind annotation required; types of kind * are promoted to kinds
-- this is essentially indistinguishable from `data Unit`
type constant Meter :: Unit
-- Here, we can define a new constant of a non-* kind. This is very useful!
type constant Second :: Unit
-- We can even pattern-match on these constants:
type family UnitToString (x :: Unit) :: Symbol where
UnitToString Meter = "m"
UnitToString Second = "m"
type constant Weird :: Nat -> Bool
-- This is OK to declare. But we *cannot* pattern-match on it, because the return
-- kind is closed.
</pre><p>
This last example may be controversial, but I think it's OK. The others are less controversial in my opinion. What this essentially does is allow for <em>open</em> datakinds.
</p>
<p>
Once these constants are declared, then a plugin can define an equational theory over them.
</p>
<p>
Unfortunately, this is a much bigger change than just allowing empty CTFs. But it somehow smells better to me.
</p>
<p>
Thoughts?
</p>
TicketadamgundryFri, 17 Apr 2015 14:56:26 GMT
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:5
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:5
<blockquote class="citation">
<p>
What Adam really wants here is the ability to create new type-level constants at arbitrary kind.
</p>
</blockquote>
<p>
Is it? Open datakinds would be nice, but <code>Symbol</code> and <code>*</code> already give us quite a lot of wriggle room.
</p>
<p>
My real problem is more in creating type-level function symbols without any equational theory, which (with <a class="ext-link" href="https://phabricator.haskell.org/D841" title="D841 in Phab"><span class="icon"></span>Phab:D841</a> at least) goes like this:
</p>
<pre class="wiki">data Unit
type family Mul (u :: Unit) (v :: Unit) :: Unit where
</pre><p>
In particular, to avoid conflict with plugin-generated axioms, <code>Mul</code>
</p>
<ul><li>must be saturated;
</li></ul><ul><li>is not injective, so <code>Mul u v ~ Mul v u</code> does not imply <code>u ~ v</code>;
</li></ul><ul><li>cannot be used in patterns;
</li></ul><ul><li>cannot be given any instances by the user (this is the only condition not satisfied by an open type family).
</li></ul><p>
I don't quite understand how your proposal would work for this case. What does it mean to declare <code>Weird</code> as a constant in a closed kind? Note that giving <code>Mul</code> kind <code>Unit -> Unit -> Unit</code> is no good, because that means it is injective (at least unless we add another flavour of type-level function space). In any case, adding a whole new declaration form feels like rather more work than my needs justify.
</p>
<p>
<a class="ext-link" href="https://phabricator.haskell.org/D841" title="D841 in Phab"><span class="icon"></span>Phab:D841</a> is a relatively simple change (deleting 7 lines of code, in its original incarnation before distinguishing abstract/empty CTFs) that is consistent with the way type families currently work. No matter how much we might wish it otherwise, type families are very different from term-level functions.
</p>
<p>
I'm happy to see a fix for <a class="new ticket" href="http://ghc.haskell.org/trac/ghc/ticket/9636" title="#9636: bug: Function with type error accepted (new)">#9636</a>, but preferably in a backwards-compatible way.
</p>
TicketgoldfireFri, 17 Apr 2015 20:17:04 GMT
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:6
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:6
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/9840#comment:5" title="Comment 5">adamgundry</a>:
</p>
<blockquote class="citation">
<blockquote class="citation">
<p>
What Adam really wants here is the ability to create new type-level constants at arbitrary kind.
</p>
</blockquote>
<p>
Is it?
</p>
</blockquote>
<p>
Yes. :) But you don't know it yet.
</p>
<p>
After posting this morning, I thought more about this. The more I thought about it, the more I liked it.
</p>
<p>
The key idea (for me) is that currently Haskell has many different forms of type-level symbol declaration (<code>data</code>, <code>newtype</code>, <code>type family</code>, <code>data family</code>, <code>type</code>, <code>class</code>, maybe more?), but perhaps these can all be rolled into one, more flexible type of declaration. (I'm not necessarily proposing to expose this to users as such, but to think of it this way.) At the moment, I'm concerned only with how these type-level symbol declarations behave in types, completely forgetting about any term-level behavior. I'm also forgetting about FC for the moment, concentrating only on Haskell.
</p>
<ul><li><code>data</code>: Declares generative, injective constants whose result kind must be <code>*</code>. Can be pattern-matched. When considered as a kind, the set of inhabitants is closed and always known.
</li><li><code>newtype</code>: Identical to <code>data</code>, except that <code>newtype</code>s are neither generative nor injective under representational equality.
</li><li><code>type family</code>: Not generative, not injective. Accordingly, must appear always saturated. (GHC's type variable application operation in types -- that is, <code>a b</code> where <code>a</code> and <code>b</code> are type variables -- assumes that the function is generative & injective. Anything that isn't must always be saturated.) These have a limited reduction behavior known to GHC. Closed type families have a fixed reduction behavior; open type families' reduction behavior can be extended. Cannot be pattern-matched against.
</li><li><code>data family</code>: Generative & injective. When considered as a kind (in the future with kind equalities) the set of inhabitants is open, but each extension of this set requires parameters to be apart from previous sets. Can be pattern-matched against.
</li><li><code>type</code>: Like a <code>type family</code>, but with even more limited behavior.
</li><li><code>class</code>: Like <code>data</code>, but the result kind must be <code>Constraint</code>.
</li></ul><p>
<a class="ext-link" href="https://phabricator.haskell.org/D202" title="D202 in Phab"><span class="icon"></span>Phab:D202</a> extends this collection with injective type families, which are like type families, but allow injectivity in some subset of its parameters.
</p>
<p>
I have wanted the following:
</p>
<ul><li>A generative, injective type constant, whose result kind is <code>*</code>. When considered as a kind, the set of inhabitants is open. Can be pattern-matched against.
</li></ul><blockquote>
<p>
This is like <code>*</code>, but still distinguished from <code>*</code>. One may argue that this is like <code>Symbol</code>, but I want to be able to hook into GHC's module system to disambiguate identically-named inhabitants. I wanted this for <code>units</code>, where I settle for declaring my extensible set of units in kind <code>*</code>. This leads to worse error messages than would be possible if I could declare a new, open kind.
</p>
</blockquote>
<ul><li>A generative, injective type constant that can <strong>not</strong> be pattern-matched against.
</li></ul><blockquote>
<p>
This is the right place for <code>Any</code>.
</p>
</blockquote>
<p>
Adam seems to want:
</p>
<ul><li>A non-generative, non-injective type-level symbol with reduction behavior unknown to GHC. This cannot be pattern-matched against.
</li></ul><blockquote>
<p>
The reduction behavior is implemented in a plugin. This type of declaration is also the correct characterization of the type-lits operators.
</p>
</blockquote>
<p>
So it seems that there are several characteristics each type-level declaration varies in:
</p>
<ul><li>Generativity (possibly different choices for nominal vs. representational equality)
</li><li>Injectivity (possibly different choice for nominal vs. representational equality, and per argument)
</li><li>Matchability (if something is matchable, it had better be generative and injective, too!)
</li><li>Open/closed
</li></ul><p>
In addition, GHC blesses type families (and type synonyms) with a limited form of reduction.
</p>
<hr />
<p>
I'm not totally sure where all of this goes, but somehow classifying this menagerie seems meaningful. It also helps to identify missing spots and to understand what is going on better. Perhaps using empty closed type families for Adam's needs and for type-lits is OK, but it isn't really what we want, according to these classifications: these type-level symbols have an unknown reduction behavior, in contrast to empty closed type families, which have a known (vacuous) reduction behavior.
</p>
TicketadamgundryFri, 24 Apr 2015 10:42:48 GMT
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:7
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:7
<p>
Thanks, Richard, it's good to try to simplify and bring order to these; I hadn't realised what a can of worms I was opening with this feature request!
</p>
<p>
In the interests of simplicity, is it actually necessary to distinguish "matchability" from generativity+injectivity? In particular, if <code>Any</code> remains non-generative (as at present) then I think the distinction collapses. The only case this matters is if we needed to conclude <code>f ~ Any : forall k . k</code> from <code>f @k0 ~ Any @k0 : k0</code>; but do we?
</p>
<p>
I think it's perhaps also helpful to divide things up along the lines of where their equational theory comes from (considering only nominal roles for now):
</p>
<ul><li>trivial equational theory (<code>data</code>, <code>newtype</code>, <code>class</code>)
</li><li>equational theory specified at declaration site (<code>type</code>, closed <code>type family</code>)
</li><li>special equational theory either built-in or provided via plugin (type lits operators, what I want)
</li><li>open equational theory that can be extended anywhere (open <code>type family</code>, <code>data family</code>)
</li></ul><p>
(The <code>data family</code> case is slightly strange, because the equational theory can be extended anywhere, but only in a very limited way.)
</p>
TicketgoldfireFri, 24 Apr 2015 12:34:10 GMT
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:8
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:8
<p>
You're right that in the current state of affairs, generativity+injectivity imply matchability. But (until <a class="ext-link" href="https://phabricator.haskell.org/D202" title="D202 in Phab"><span class="icon"></span>Phab:D202</a> lands) generativity also implies injectivity and vice versa. What characteristics to track separately is one of the challenges here...
</p>
<p>
Suppose units-of-measure annotations were represented by a type headed <code>UnitExp</code>. <code>UnitExp</code> would not be injective, because it would take as arguments information about the different units and their powers, and this information has a non-trivial equational theory. However, <code>UnitExp</code> would, assumedly, be generative, in that no non-<code>UnitExp</code>s would ever be the same as a <code>UnitExp</code>. I don't know exactly what this means to the issue above, but it's an example of something that's generative but not injective.
</p>
<p>
Yes, I completely agree about distinguishing based on equational theory. And the <code>data family</code> case is quite interesting, I think, because it shows how these concepts can be combined in unusual ways: data families are generative+injective, but yet have a non-trivial and extensible equational theory. If they didn't already exist, I would probably say this point in the space didn't exist! So there's something to be learned from them.
</p>
<p>
Also, in case I haven't made this clear: these musings probably don't belong in this ticket, as I don't think these ideas should hold anything up about empty closed type families. But I'm hoping this leads to a slightly cleaner solution down the road.
</p>
TicketAdam Gundry <adam@…>Mon, 04 May 2015 14:41:23 GMT
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:9
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:9
<p>
In <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/4efa421327cf127ebefde59b2eece693e37dc3c6/ghc" title="Permit empty closed type families
Fixes #9840 and #10306, and ...">4efa421327cf127ebefde59b2eece693e37dc3c6/ghc</a>:
</p>
<pre class="message">Permit empty closed type families
Fixes #9840 and #10306, and includes an alternative resolution to #8028.
This permits empty closed type families, and documents them in the user
guide. It updates the Haddock submodule to support the API change.
Test Plan: Added `indexed-types/should_compile/T9840` and updated
`indexed-types/should_fail/ClosedFam4` and `th/T8028`.
Reviewers: austin, simonpj, goldfire
Reviewed By: goldfire
Subscribers: bgamari, jstolarek, thomie, goldfire
Differential Revision: https://phabricator.haskell.org/D841
GHC Trac Issues: #9840, #10306</pre>
TicketadamgundryMon, 04 May 2015 14:49:02 GMTstatus changed; testcase set
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:10
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:10
<ul>
<li><strong>status</strong>
changed from <em>patch</em> to <em>merge</em>
</li>
<li><strong>testcase</strong>
set to <em>indexed-types/should_compile/T9840</em>
</li>
</ul>
TicketthoughtpoliceMon, 11 May 2015 12:03:45 GMT
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:11
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:11
<p>
So, this one visibly changes the API and requires a Haddock update, so I'm pretty inclined to leave it as is and not merge. Adam, is this one critical, or can it be worked around/backported reasonably?
</p>
TicketadamgundryMon, 11 May 2015 12:05:58 GMTstatus changed; resolution, milestone set
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:12
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:12
<ul>
<li><strong>status</strong>
changed from <em>merge</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
<li><strong>milestone</strong>
set to <em>7.12.1</em>
</li>
</ul>
<p>
On reflection, I agree, let's leave this in HEAD but not merge into 7.10.
</p>
TicketthoughtpoliceFri, 11 Sep 2015 08:38:26 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:13
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:13
<ul>
<li><strong>milestone</strong>
changed from <em>7.12.1</em> to <em>8.0.1</em>
</li>
</ul>
<p>
Milestone renamed
</p>
TicketadamgundryFri, 18 May 2018 14:03:13 GMTkeywords set
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:14
http://ghc.haskell.org/trac/ghc/ticket/9840#comment:14
<ul>
<li><strong>keywords</strong>
<em>TypeCheckerPlugins</em> added
</li>
</ul>
Ticket