Add kind polymorphism. #563

sellout · 2018-09-06T23:44:17Z

I wanted to propose this before I spend too much time on it, so let me know if
it’d be acceptable in some form. (And it would also require a change to the
language spec.)

Here’s an example:

./polyfunctor

  λ(j : Kind)
→ λ(k : Kind)
→ λ(c : j → j → Type)
→ λ(d : k → k → Type)
→ λ(f : j → k)
→ { map : ∀(a : j) → ∀(b : j) → c a b → d (f a) (f b) }

then

./polyfunctor
Type
Type
(λ(a : Type) → λ(b : Type) → a → b)
(λ(a : Type) → λ(b : Type) → a → b)
Optional

normalizes to

{ map : ∀(a : Type) → ∀(b : Type) → (a → b) → Optional a → Optional b }

and

./polyfunctor
(Type → Type)
(Type → Type)
(λ(a : Type → Type) → λ(b : Type → Type) → ∀(i : Type) → a i → b i)
(λ(a : Type → Type) → λ(b : Type → Type) → ∀(i : Type) → a i → b i)

normalizes to

  λ(f : (Type → Type) → Type → Type)
→ { map :
        ∀(a : Type → Type)
      → ∀(b : Type → Type)
      → (∀(i : Type) → a i → b i)
      → ∀(i : Type)
      → f a i
      → f b i
  }

I wanted to propose this before I spend too much time on it, so let me know if it’d be acceptable in some form. (And it would also require a change to the language spec.) Here’s an example: ./polyfunctor ```dhall λ(j : Kind) → λ(k : Kind) → λ(c : j → j → Type) → λ(d : k → k → Type) → λ(f : j → k) → { map : ∀(a : j) → ∀(b : j) → c a b → d (f a) (f b) } ``` then ```dhall ./polyfunctor Type Type (λ(a : Type) → λ(b : Type) → a → b) (λ(a : Type) → λ(b : Type) → a → b) Optional ``` normalizes to ```dhall { map : ∀(a : Type) → ∀(b : Type) → (a → b) → Optional a → Optional b } ``` and ```dhall ./polyfunctor (Type → Type) (Type → Type) (λ(a : Type → Type) → λ(b : Type → Type) → ∀(i : Type) → a i → b i) (λ(a : Type → Type) → λ(b : Type → Type) → ∀(i : Type) → a i → b i) ``` normalizes to ```dhall λ(f : (Type → Type) → Type → Type) → { map : ∀(a : Type → Type) → ∀(b : Type → Type) → (∀(i : Type) → a i → b i) → ∀(i : Type) → f a i → f b i } ```

sellout · 2018-09-06T23:55:47Z

Just to have a non-endofunctor:

./polyfunctor
(Type -> Type)
Type
(λ(a : Type → Type) → λ(b : Type → Type) → ∀(i : Type) → a i → b i)
(λ(a : Type) → λ(b : Type) → a → b)

normalizes to

  λ(f : (Type → Type) → Type)
→ { map :
        ∀(a : Type → Type)
      → ∀(b : Type → Type)
      → (∀(i : Type) → a i → b i)
      → f a
      → f b
  }

(which is the “kind” of thing I would use in dada for mapping over fixed-point operators).

Gabriella439 · 2018-09-07T15:37:01Z

@sellout: Yes, I'll accept this. The main benefit of this (which you appear to have noticed while implementing this) is that it allows records of types with mixed kinds (i.e. { foo = List, bar = Bool }) since they can now be encoded using kind-polymorphism. That in turns means that most packages will only need to export at most two records: one for terms and one for types.

It also doesn't affect existing user code

Profpatsch · 2018-09-07T19:30:40Z

is that it allows records of types with mixed kinds (i.e. { foo = List, bar = Bool }) since they can now be encoded using kind-polymorphism

If we can do that step, what’s the problem with doing the same for values as well? That the type system would need to become dependent in the process?

sellout · 2018-09-07T20:21:39Z

Then how would you feel about universes? And maybe universe polymorphism? 😆

Gabriella439 · 2018-09-07T20:28:43Z

@Profpatsch: No, separating types and terms in records is independent of whether or not the type system is dependent. In other words, even if we turned on dependent types we would still need to keep types and terms separate.

Basically all of Dhall's higher-level features (like builtins, records, lists, unions, etc.) can be encoded in terms of lower-level features (i.e. pure lambda calculus) using Dhall's own type system.

For example, a record of the form:

{ foo = 1, bar = True }

... could be encoded like this:

λ(result : Type) → λ(makeRecord : ∀(foo : Natural) → ∀(bar : Bool) → result) → makeRecord 1 True

... and accessing a field of a record like that:

λ(r : { foo : Natural, bar : Bool }) → r.foo

... could be encoded like this:

  λ(r : ∀(result : Type) → (∀(foo : Natural) → ∀(bar : Bool) → result) → result)
→ r Natural (λ(foo : Natural) → λ(bar : Bool) → foo)

The encoding might be very clumsy to use and might be less efficient, but it's theoretically possible to translate all of Dhall's features to raw System Fω.

The reason these encodings are important is that they establish that Dhall's higher-level features are still sound and non-Turing-complete since they can be translated to a non-Turing-complete language (System Fω in this case).

The reason this feature is sometimes confused with dependent types is because if you don't have a sound way to translate records to the underlying lambda calculus then records become a backdoor that you can use to break the type system. One example of that breaking the type system was using records to make code accidentally dependently typed, but that's not the only possible way that it can break the type system.

As @sellout just mentioned, if you want to have records that mix types and terms, then what you actually need is universe polymorphism in order to be able to encode records of types and terms in lambda calculus. Universe polymorphism means that instead of Type, Kind, and Sort we would have Type 0, Type 1, Type 2, ... or more generally we could parametrize the constant by a natural number. If you have that then you gain the ability to mix records of types and terms in a sound way. If I remember correctly, a record like this:

{ foo = 1, bar = Natural }

... would translate to:

λ(n : Natural) → λ(result : Type n) → λ(makeRecord : ∀(foo : Natural) →∀(bar : Type) → result) →makeRecord 1 Natural

@sellout: I'm not sure about that yet. Let me spend some time reasoning through how it's encoded and how that would affect the type-checking rules for records (and how to do it in a way that doesn't break existing user code).

Gabriella439 · 2018-09-10T00:15:59Z

@sellout: So the issue with using universe polymorphism is that you can't hide it from the user when type-checking record types. The issue you run into is that the type of a record type would end up being polymorphic over the universe and you wouldn't be able to hide that universe-polymorphism from the end user for a mixed record of terms and types.

For example, under the current type system, the type of the type of a record of terms is Type and the type of the type of a record of types is Kind. If you introduce universe polymorphism then the type of a mixed record of terms and types would be ∀(n : Natural) → Type n, which means that the user would need to explicitly instantiate the record ahead of time to a specific universe in order to use it anywhere that expected either a Type 0 or a Type 1. Also, once you instantiated it to such a universe you would only be able to extract either terms (if you instantiated it to Type 0) or types (if you instantiated it to Type 1) but no longer both.

Let me motivate this with a concrete example with the following type-level function:

-- ./Map.dhall
--
-- Simulate a map as an association list

λ(type : { key : Type, value : Type }) → List { key : type.key, value : type.value }

$ dhall <<< './Map.dhall { key = Text, value = Natural }'
List { key : Text, value : Natural }

The interpreter (correctly) does not flag ./Map.dhall as a dependent type because the type system infers that the type of { key : Type, value : Type } is Kind so the ./Map.dhall is treated as an ordinary type constructor that just happens to permit initializing its type variables using record syntax instead of positional type arguments.

However, now imagine that you have a record with these contents:

{ key = Text, value = Natural, x = 0 }
  : { key : Type, value : Type, x : Natural }
  : ∀(n : Natural) → Type n

... which could potentially be used as either a record of terms or types. The user would need to explicitly instantiate it to a record of types before they could pass it to ./Map.dhall so that you don't accidentally create a dependent-types backdoor where they could thread terms like the field x into the type (not that dependent types are bad, but this is an example of what could accidentally could go wrong if you don't make the universe explicit for such a mixed record). More generally, if you don't require the user to be explicit about the choice of universe for mixed records then I believe a similar trick could be used as a backdoor to synthesize the unsound Type n : Type n.

So I think the best we'll be able to do for the foreseeable future is your original proposal to add Sort and then for users to export one record for terms and another record for types. I can then document the two-export idiom in the Dhall wiki as a work-around for the type system limitation.

There's another related issue I considered alongside this one, which is the proposal you raised earlier for dependent records. I think that even if we don't support universe polymorphism it doesn't preclude the possibility of dependent records. The reason why is that in the vast majority of use cases for dependent records (i.e. modules with scoped access to the ordered record fields) you usually always want the final result of the scoped access to be a term (or another module), so the type of the type of a dependent record can be fixed to Type and you can treat it as a record of terms for the purposes of passing the module around opaquely.

sellout · 2018-09-16T17:51:09Z

If you introduce universe polymorphism then the type of a mixed record of terms and types would be ∀(n : Natural) → Type n

Is this necessarily true? I may be out of my depth here, but I was thinking that effectively Type would be an alias for U 0, and Kind for U 1, and just as

{ key : Type, value : Type, x : Natural } : Kind

isn’t valid with kind polymorphism, universe polymorphism wouldn’t necessarily allow

{ key : U 0, value : U 0, x : Natural } : U 1

With universe polymorphism, I was hoping to be able to to do something roughly like

-- pattern functor for lists
  λ(level : Level)
→ λ(a : U level)
→ λ(b : U level)
→   < Nil : ({} : U level)
    | Cons : { head : a, tail : b }
    >
  : U level

to enable HLists, etc.

Gabriella439 · 2018-09-16T23:02:38Z

@sellout: So I looked into this more closely and it looks like in Agda the way they do this is that the universe level represents an upper bound on the type of the type of the value that you can extract from a record. Specifically, if the type of the type of A is Universe m and the type of the type of B is Universe n then the type of the type of A x B is Universe (max m n). That implies that the type of the type of a record is the type of the type of the "largest" field that you could possibly extract.

However, I think that if you want this for heterogeneous lists then it sounds like what you want is metaprogramming which I think would be solved better by access to the abstract syntax tree rather than implementing it with the language. The reason why is that if you implement heterogeneous lists within the language you are going to lose all the syntactic niceties and features of Dhall records which you could keep if you access the record structure through the Haskell API.

phadej · 2018-10-03T00:27:43Z

I think this is bad idea.

% cat example.dhall
λ(j : Kind) → λ(a : Kind → Kind) → λ(b : Kind) → a (a b)

% cat example.dhall | dhall type
∀(j : Kind) → ∀(a : Kind → Kind) → ∀(b : Kind) → Kind

https://en.wikipedia.org/wiki/System_U#Girard's_paradox

The definitions of System U and U− allow the assignment of polymorphic kinds to generic constructors in analogy to polymorphic types of terms in classical polymorphic lambda calculi, such as System F. An example of such a generic constructor might be[2]:353 (where k denotes a kind variable)

as above

This mechanism is sufficient to construct a term with the type forall (p : Type) -> p, which implies that every type is inhabited.

A simplification of Girard's paradox by Antonius J. C. Hurkens
have an example of the bottom value. I tried to make it, but I'm too tired, here's the start

   let bottom = forall (any : Type) -> any
in let not = \(p : Type) -> bottom
in let pow = \(X : Kind) -> X -> Type
in let U = forall (X : Kind) -> (pow (pow X) -> X) -> pow (pow X)

in let tau : pow (pow U) -> U
         = \(t : pow (pow U)) ->
           \(X : Kind) ->
           \(f : pow (pow X) -> X) ->
	   \(p : pow X) ->
	   (t (\(x : U) -> p (f ((x X) f))))

in let sigma : U -> pow (pow U)
             = \(s : U) ->
               ((s U) (\(t : pow (pow U)) -> tau t))

in let Delta : pow U
             = \(y : U) ->
               not (forall (p : pow U) -> ((sigma y) p) -> (p (tau (sigma y))))

in let Omega : U
             = tau (\ (p : pow U) -> forall (x : U) -> (((sigma x) p) -> p x))

in \(t : pow (pow U)) -> sigma (tau t)

Gabriella439 · 2018-10-03T01:32:12Z

@phadej: @sellout's proposal does not entail Girard's paradox. To be precise, neither kind polymorphism nor universe polymorphism imply Girard's paradox.

I'm familiar with the issues with System U and Type : Type, but that's not what is being proposed here.

sellout · 2018-10-05T00:35:55Z

Now that the spec change is merged (dhall-lang/dhall-lang#238), what’s the the plan for this? More changes to be made?

I’ve written tons of code using this branch:

sellout · 2018-10-05T00:37:23Z

And I noticed it just failed … but I can’t figure out what I broke from the log.

f-f

I'm not sure what's my opinion on this (I mean the whole special casing Sort vs having Universe n at least under the hood for simplicity of standardization/implementation), so my only comment about this PR will be: looks good but let's add some normalization and typechecking tests that exercise the new feature 👍

sellout · 2018-10-05T14:21:31Z

@f-f Good point. I can copy over some stuff from the other repos I linked.

Gabriella439 · 2018-10-05T15:26:43Z

@sellout: The failure was a transient issue. I restarted the build and it passes now.

Gabriella439 · 2018-10-07T13:15:06Z

@sellout: Once the corresponding change to the spec is merged you have the greenlight to merge this. As far as I can tell the only outstanding request is to add tests like @f-f suggested

sellout · 2018-10-07T15:22:13Z

Cool. I’m moving today, but hopefully can add the tests early this week.

Gabriella439 · 2018-10-07T19:46:31Z

I ran into one issue when testing this branch, which is that a record like { x = List } still does not type-check. However, I realized that technically the standard had the same issue so fixing it requires a change to the standard:

dhall-lang/dhall-lang#241

And test it.

Gabriella439 · 2018-10-14T19:09:23Z

This looks good to me. Did you have any other changes planned?

sellout · 2018-10-14T22:32:14Z

@Gabriel439 Yeah, I noticed (when writing tests) that Sort doesn’t parse as a reserved word. I think I lost that when the parsing restructuring went in. But adding the obvious places didn’t fix that (it still says “Error: Unbound variable: Sort”), so I gotta sit and stare a bit tonight. But I’ll merge it today, with some new tests.

Gabriella439 · 2018-10-14T22:33:31Z

@sellout: If you're busy, just add a failing test and I can fix things so that the test passes

One fails because `Sort` isn’t parsed correctly. I added `Sort` to the “obvious” places in the parser, but that’s not cutting it. Not sure if it’s something like trying to parse `Some` and then failing to backtrack or what. Also made a small change to the parser tests, since previously they were all getting grouped under “whitespace”, and I don’t think that was correct.

…into kind-polymorphism

sellout · 2018-10-15T03:44:08Z

@Gabriel439 Ok, I pushed the failing test, along with other stuff.

This still required removing the test for type-checking `Kind → Kind` since `Sort` is not valid as a type annotation (since it has no type of its own) I replaced it with a test for parsing `Sort` and instead did an ad-hoc verification that `Kind → Kind` had an inferred type of `Sort`

Gabriella439 · 2018-10-15T15:26:43Z

@sellout: I have a pull request up here for the fix to your branch: sellout#1

Fix parsing of `Sort`

sellout added 2 commits September 6, 2018 18:26

Fix some compilation errors that didn’t explode things locally.

dd188f0

Fix some places that didn’t allow kind variables.

ed2728b

Gabriella439 mentioned this pull request Sep 11, 2018

treat directories as records dhall-lang/dhall-lang#139

Closed

sellout mentioned this pull request Sep 16, 2018

Is there a wildcard for pattern matching? #574

Closed

Clean up.

6163cf7

sellout added 2 commits October 4, 2018 14:34

More cleanup.

df9bedd

Merge remote-tracking branch 'upstream/master' into kind-polymorphism

6f167c0

f-f reviewed Oct 5, 2018

View reviewed changes

Merge branch 'master' into kind-polymorphism

6e12447

Gabriella439 mentioned this pull request Oct 13, 2018

Version 1.17.0 → 1.18.0 #636

Merged

sellout added 2 commits October 12, 2018 21:18

Merge remote-tracking branch 'upstream/master' into kind-polymorphism

233b84c

Fix the issue with RecordLits containing types of multiple kinds.

15485ee

And test it.

Gabriella439 approved these changes Oct 14, 2018

View reviewed changes

Merge branch 'master' into kind-polymorphism

0a468f9

sellout added 2 commits October 14, 2018 21:39

Merge branch 'kind-polymorphism' of github.com:sellout/dhall-haskell …

25aab6b

…into kind-polymorphism

sellout added 2 commits October 15, 2018 09:30

Merge pull request #1 from dhall-lang/sellout-kind-polymorphism

1ec951d

Fix parsing of `Sort`

Fix sort test file name.

fc2f617

sellout merged commit 2010d41 into dhall-lang:master Oct 15, 2018

f-f mentioned this pull request Oct 22, 2018

Hurkens' paradox? dhall-lang/dhall-lang#250

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add kind polymorphism. #563

Add kind polymorphism. #563

sellout commented Sep 6, 2018

sellout commented Sep 6, 2018

Gabriella439 commented Sep 7, 2018

Profpatsch commented Sep 7, 2018

sellout commented Sep 7, 2018

Gabriella439 commented Sep 7, 2018

Gabriella439 commented Sep 10, 2018

sellout commented Sep 16, 2018

Gabriella439 commented Sep 16, 2018

phadej commented Oct 3, 2018

Gabriella439 commented Oct 3, 2018

sellout commented Oct 5, 2018

sellout commented Oct 5, 2018

f-f left a comment •

edited

Loading

sellout commented Oct 5, 2018

Gabriella439 commented Oct 5, 2018

Gabriella439 commented Oct 7, 2018

sellout commented Oct 7, 2018

Gabriella439 commented Oct 7, 2018

Gabriella439 commented Oct 14, 2018

sellout commented Oct 14, 2018

Gabriella439 commented Oct 14, 2018

sellout commented Oct 15, 2018

Gabriella439 commented Oct 15, 2018

Add kind polymorphism. #563

Add kind polymorphism. #563

Conversation

sellout commented Sep 6, 2018

sellout commented Sep 6, 2018

Gabriella439 commented Sep 7, 2018

Profpatsch commented Sep 7, 2018

sellout commented Sep 7, 2018

Gabriella439 commented Sep 7, 2018

Gabriella439 commented Sep 10, 2018

sellout commented Sep 16, 2018

Gabriella439 commented Sep 16, 2018

phadej commented Oct 3, 2018

Gabriella439 commented Oct 3, 2018

sellout commented Oct 5, 2018

sellout commented Oct 5, 2018

f-f left a comment • edited Loading

Choose a reason for hiding this comment

sellout commented Oct 5, 2018

Gabriella439 commented Oct 5, 2018

Gabriella439 commented Oct 7, 2018

sellout commented Oct 7, 2018

Gabriella439 commented Oct 7, 2018

Gabriella439 commented Oct 14, 2018

sellout commented Oct 14, 2018

Gabriella439 commented Oct 14, 2018

sellout commented Oct 15, 2018

Gabriella439 commented Oct 15, 2018

f-f left a comment •

edited

Loading