Opened 4 years ago

Last modified 18 months ago

#11080 new feature request

Open data kinds

Reported by: dmcclean Owned by:
Priority: low Milestone:
Component: Compiler Version:
Keywords: Cc: Iceland_jack, lelf, goldfire, jstolarek, int-index, kosmikus, alpmestan
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #6024 Differential Rev(s): Phab:D1778
Wiki Page: GhcKinds/KindsWithoutData

Description

When we need type level symbols, we used to only have one option, EmptyDataDecls. The symbolic type parameters would be given kind *, but the convention would be to use types that are (mostly) uninhabited and that were made for the purpose of serving as symbols. For an example of this see http://hackage.haskell.org/package/servant-0.4.4.5/docs/Servant-API-ContentTypes.html.

Now we also have the Symbol kind which can serve a similar purpose.

Neither of these options is fully satisfactory for examples like servant's type-level encoding of content types, or the units libraries type-level encoding of physical dimensions, for the following reasons:

We would prefer to give these types a kind other than * both because they are uninhabited and because we wish to provide documentation of what types are acceptable in these parameter positions.

But the only facility we have for creating new kinds is DataKinds, and the kinds it creates are all closed. This is problematic because we wish to allow client modules to declare new content types or new physical dimensions. We could provide "newkind" wrappers around Symbol using DataKinds, but that runs in to name collision issues. The EmptyDataDecls solution is superior here because types with the same name declared in different modules remain distinct.

Instead I propose the addition of a new feature where data kinds can be open.

In a discussion at https://github.com/bjornbm/dimensional-dk/issues/96 in which @goldfire participated, we arrived at the following proposal for concrete syntax, but certainly there are many possible variations one could imagine which might have equal or greater merit:

-- declares a new kind which initially has no inhabitants
data open ContentType

-- declares a new type of kind ContentType, which is distinct
-- from any others that may have been declared elsewhere,
-- even if they have the same non-module-qualified name
data constructor JSON :: ContentType

(@goldfire raised the possibility of one day interpreting the same data constructor ... syntax at the type level to declare inhabited types for which some constructors are defined in one module but which are open to extension with new constructors by other modules, but that is a distinct issue in all other ways apart from possibly wishing to share syntax.)

Change History (18)

comment:1 Changed 4 years ago by jstolarek

Cc: jstolarek added

comment:2 Changed 4 years ago by goldfire

Simon PJ, Stephanie Weirich, Andres Löh, Kenny Foner, and I discussed this recently, and we didn't spot any problems with the proposal, neither in terms of theory nor implementation.

  • Question: can open kinds be parameterized? Answer: Yes. Example:
    data open Dimension :: *
    data constructor Length :: Dimension
    data open Unit :: Dimension -> *
    data constructor Meter :: Unit 'Length
    data constructor Foot :: Unit 'Length
    
  • Alternative syntax: data constructor is noisy. Just omit, allowing a declaration like Length :: Dimension. Objection: this overlaps with a naked top-level Template Haskell splice.
  • Alternative syntax: data constructor is noisy. How about this:
    data open Unit :: *
    data extension Unit where
      Meter :: Unit
      Foot :: Unit
    

My (Richard's) objection: But this grouping of Meter and Foot is meaningless. Breaking up the group is the same as grouping. It's just syntactic. But this isn't a hard objection if others like the idea.

  • Related topic: What about other design points as explored in comment:6:ticket:9840? In particular, how does this relate to non-generative, non-injective symbols whose equational theory is given by a plugin? (Non-generative, non-injective symbols whose equational theory is given by GHC are known as type families.) Defining such a symbol was the point of #9840 to begin with, and we settled on an empty closed type family as the nearest approximation. After some discussion, it seemed that the open kind proposal was separate enough that these don't need to be considered together. But a suggestion for a unifying syntax would be welcome!

Bottom line: let's do it, once we decide on a syntax. I still favor the syntax proposed, with data constructor. Other opinions are welcome.

comment:3 Changed 4 years ago by jstolarek

Can I join in? I'd like to work on the implementation. Unless someone has already volunteered?

comment:4 Changed 4 years ago by dmcclean

I'm not sure who you're asking, but I'll weigh in that as far as I know nobody has begun any implementation work yet and your contribution would probably be welcome. Personally implementing this is way over my head, so I can't offer to help myself.

I do like the alternative syntax proposal data Extension Unit where .... It's true that the grouping is semantically meaningless, but it does seem more similar to existing syntax. Also if this were to later be extended to allow adding new constructors to open types of kind * this syntax would seem to more naturally support adding new GADT style constructors.

comment:5 Changed 4 years ago by goldfire

The next step should be making a formal proposal on the wiki and gathering comments about concrete syntax and such. No one has yet formally volunteered to implement, though I was thinking about it. Happy to cede, though. Thanks!

As a response to @dmcclean: The original data constructor syntax works well with GADT constructors, because the full type of the constructors is included after the ::. I still favor my original syntax, but it already looks like I'm in the minority. :)

comment:6 Changed 4 years ago by jstolarek

Owner: set to jstolarek

Note that we also have #6024 (and its wiki page GhcKinds/KindsWithoutData), which is about implementing close data kinds without the need for declaring a data type. Can we implement this and #6024 at the same time? It seems to me that the answer is yes.

Here is my proposal for the syntax:

-- (1) closed kinds, normal syntax
kind Universe = Sum  Universe Universe
              | Prod Universe Universe
              | K *

-- (2) closed kinds, GADT syntax.
kind Universe where
   Sum  :: Universe -> Universe -> Universe
   Prod :: Universe -> Universe -> Universe
   K    :: *                    -> Universe

-- (3) open kinds
kind open Universe
kind member Sum  :: Universe -> Universe -> Universe
kind member Prod :: Universe -> Universe -> Universe
kind member K    :: *                    -> Universe

This syntax would steal kind as a keyword. Do we feel bad about it? Importantly, do we put this new feature into its own language extension or do we make it part of DataKinds? If the former then I don't feel bad about stealing kind, as we won't break any of the existing code. But if we put this into DataKinds then I might reconsider my preference for syntax. Then again I still would rather break backwards compatibility and have nice syntax then construct verbose syntax for the sake of backwards compatibility. Also, I don't like data constructor syntax. I find it misleading as data constructor is a totally different thing than what we are declaring (in fact, in #6024 we specifically wish to avoid creating data constructors).

If we made this into a separate language extension, I wonder if that extension would have to be enabled only in modules that declare kinds or also in the ones that use them?

How does this feature interact with * :: *? In #6024 dreixel says: "[in the future] types and kinds might be collapsed into a single level. That would also destroy the possibility of doing what is asked in this ticket, though." I believe that dreixel's line of reasoning was this:

When we declare kind K = T, then K is a kind a T is a type. But since types and kinds are now the same then we must be able to treat K as a type, which makes T a value and thus we arrived at declaring a data type.

If this was what dreixel meant then I disagree with it. It's like saying that since Int :: *, then * can be treated as a type and thus Int can be treated as a value (whatever that would mean).

Another question related to * :: * is about namespace collision. If I say:

-- assume DataKinds are enabled, so that C becomes a type
data T = C

kind K = T | C

do we have collisions beetwen definitions of Ts and Cs? They are all in namespace of types. On the other hand they could be disambiguated by kind, but I'm not sure if this is acceptable.

Aside: if we can index kinds does this mean we have sort polymorphism?

I will work on extending GhcKinds/KindsWithoutData wiki page, as I think this discussion belongs there (even if closed and open kinds should be implemented separately). Yell if you think otherwise.

Last edited 4 years ago by jstolarek (previous) (diff)

comment:7 in reply to:  6 Changed 4 years ago by goldfire

Replying to jstolarek:

Note that we also have #6024 (and its wiki page GhcKinds/KindsWithoutData), which is about implementing close data kinds without the need for declaring a data type. Can we implement this and #6024 at the same time? It seems to me that the answer is yes.

Agreed. That would be nice.

Here is my proposal for the syntax: ...

This syntax would steal kind as a keyword. Do we feel bad about it?

I think it's easily avoidable, by just writing data kind. Using just kind here could be confusing, because your kind is not at all analogous to Haskell's type.

Also, I don't like data constructor syntax. I find it misleading as data constructor is a totally different thing than what we are declaring (in fact, in #6024 we specifically wish to avoid creating data constructors).

We are precisely declaring a data constructor. It's just a data constructor that makes compile-time data. I recognize that others may usefully disagree about the meaning of a data constructor here, but I really to think that these are data constructors. (Compare to what other dependently typed languages do.)

If we made this into a separate language extension, I wonder if that extension would have to be enabled only in modules that declare kinds or also in the ones that use them?

Only at declaration sites. Infectious extensions are annoying.

... If this was what dreixel meant then I disagree with it.

I agree with you. * :: * does not obviate this or #6024.

Another question related to * :: * is about namespace collision. If I say:

-- assume DataKinds are enabled, so that C becomes a type
data T = C

Ah. But C does not become a type. C lives in the data namespace. It's just that the renamer looks in both the type namespace and then the data namespace. C is always just a data constructor, even when used in a type.

kind K = T | C

do we have collisions beetwen definitions of Ts and Cs? They are all in namespace of types. On the other hand they could be disambiguated by kind, but I'm not sure if this is acceptable.

You are suggesting type-directed name resolution. That's a bigger pickle than we need to crack at the moment.

Aside: if we can index kinds does this mean we have sort polymorphism?

No no no. We have type polymorphism. And that's it. There are no kinds and no sorts. Just types. We humans have small brains and it is thus helpful to use both kind and type in speech to keep the ideas apart. But the terms are now truly synonymous. So, a type that classifies a type can be indexed, perhaps polymorphically. But let's not call it sort polymorphism. :)

I will work on extending GhcKinds/KindsWithoutData wiki page, as I think this discussion belongs there (even if closed and open kinds should be implemented separately). Yell if you think otherwise.

Fine by me. Thanks!

comment:8 Changed 4 years ago by jstolarek

I updated the wiki page.

comment:9 Changed 4 years ago by jstolarek

Differential Rev(s): Phab:D1778
Wiki Page: GhcKinds/KindsWithoutData

comment:10 Changed 4 years ago by jstolarek

Two design questions:

  1. This work should obviously go into its own language extension. How should we name it? Note that it will enable not only open data kinds, but also closed data kinds without associated data type (#6024)
  1. Should the new extension imply any other extensions? I think PolyKinds should be implied.

comment:11 Changed 4 years ago by goldfire

Despite the work you've done on this, I am becoming less convinced that we should fix #6024. Reading the code, I realized that this extension would allow users to define data constructors that live only in types, but there's no way to make one that lives only in terms! That seems oddly asymmetrical. It might be worth a wider discussion about the merits of kind-only datatypes in GHC 8.x.

Of course, none of this applies to open kinds, which are indeed still very useful.

comment:12 Changed 3 years ago by lelf

Cc: lelf added

comment:13 Changed 3 years ago by int-index

Cc: int-index added

comment:14 Changed 3 years ago by kosmikus

Cc: kosmikus added

comment:15 Changed 3 years ago by Iceland_jack

Cc: Iceland_jack added

comment:16 Changed 2 years ago by alpmestan

Cc: alpmestan added

comment:17 Changed 22 months ago by Iceland_jack

I discuss my use cases for this feature here Encoding Overlapping, Extensible Isomorphisms & Rethinking Tricky Classes: Explicit Witnesses of Monoid Actions, Semigroup / Monoid / Applicative homomorphisms.


Any problems with instances of open kinds

data open ContentType

data constructor JSON :: ContentType
data constructor HTML :: ContentType

class    Str (a::ContentType) where str :: String
instance Str JSON             where str = "JSON"
instance Str HTML             where str = "HTML" 

or associated types of open kinds?

class C a where
  type Content a :: ContentType

instance C Int where
  type Content Int = JSON

or marking Content injective?


This will presumably work with

type family
  Equal (a::k) (b::k) :: Bool where
  Equal a a = 'True
  Equal _ _ = 'False

where Equal JSON HTML reduces to 'False.

Last edited 22 months ago by Iceland_jack (previous) (diff)

comment:18 Changed 18 months ago by jstolarek

Owner: jstolarek deleted
Note: See TracTickets for help on using tickets.