Dhall-haskell: The new union access is not transitive across record field

[jneira]

This dhall definition works as intended:

let Scope = < Public : {} | Private : {} >
in Scope.Public {=}

However, puting the union in a record field doesnt work (at least as i expected):

let Scope = < Public : {} | Private : {} >
let types = { Scope = Scope }
in types.Scope.Public {=}

It throws:

Use "dhall --explain" for detailed errors

 Error : Not a record or a union

   types.Scope.Public
(stdin):3:4

[jneira]

Well. it seems this was already discussed in the pr. So, would be an alternative to dhall-to-cabal usage of records of unions taking in account that constructors will not work when it is equal to id?

[jneira]

Adding a let with the record field makes it work too:

let Scope = < Public : {} | Private : {} >
let types = { Scope = Scope }
let MyScope = types.Scope
in MyScope.Public {=}

I feel that behaviour it is not very intuitive :thinking:

[Gabriel439]

@jneira: The standard permits what you are trying to do. This is just a bug in the Haskell implementation since it is not complying with the standard. I believe I can fix this pretty easily before cutting the next release.

[Gabriel439]

Fix is up here: https://github.com/dhall-lang/dhall-haskell/pull/694

I will merge that before cutting the release tonight if nobody objects

[jneira]

Just tested with dhall-to-cabal and it works fine, thanks @Gabriel439
However you cant nest the record of unions in another record. This code:

let types = { Scopes = < Public : {} | Private : {} >}
let prelude = { types = types }
in prelude.types.Scopes.Public {=}

fails with

 Use "dhall --explain" for detailed errors
 Error: Invalid field
              { types = types }

explained:

You provided a record literal with a field named:
↳ types
... whose value is:
↳ { Scopes = < Private : {} | Public : {} > }
... which is not a term or ❰Type❱

This one follows the new dhall spec?
In that case we'll have to separate types from values in dhall-to-cabal prelude.

[ocharles]

Yep, that's correct - you can no longer have mixed records.

On Thu, 22 Nov 2018, 7:24 am Javier Neira <[email protected] wrote:

Just tested with dhall-to-cabal and it works fine, thanks @Gabriel439
https://github.com/Gabriel439
However you cant nest the record of unions in another record. This code:

let types = { Scopes = < Public : {} | Private : {} >}
let prelude = { types = types }
in prelude.types.Scopes.Public {=}

fails with

Use "dhall --explain" for detailed errors
Error: Invalid field
{ types = types }

explained:

You provided a record literal with a field named:
↳ types
... whose value is:
↳ { Scopes = < Private : {} | Public : {} > }
... which is not a term or ❰Type❱

This one follows the new dhall spec?
In that case we'll have to separate types from values in dhall-to-cabal
prelude.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
https://github.com/dhall-lang/dhall-haskell/issues/692#issuecomment-440936349,
or mute the thread
https://github.com/notifications/unsubscribe-auth/AABRjgyKsl1FdNXZhFOMcDQYRPQd8Tc0ks5uxlESgaJpZM4YsxCD
.

[Gabriel439]

Actually, it's disallowed for a different reason. To explain why, I'll need to specify some terminology:

• "x is a type" (with a lower-case "t") means that the type of the type of x is Kind
• "x is a kind" (with a lower-case "k") means that the type of the type of x is Sort
• "x is a Type" (with an upper-case "T") means that the type of x is Type
• "x is a Kind" (with an upper-case "K") means that the type of x is Kind

All Kinds are kinds and all Types are types, but the converse is not necessarily true: not all types are Types and not all kinds are Kinds. For example:

• List is a type, but not a Type:

  List : Type → Type : Kind
  

• { x = Bool } is a kind, but not a Kind:

  { x = Bool } : { x : Type } : Sort  -- In version 4.0.0 of the standard
  

Carefully note that in version 3.0.0 of the standard a record of types was treated as a type instead of a kind:

```haskell
{ x = Bool } : { x : Type } : Kind  -- In version 3.0.0 of the standard
```

One of the necessary changes to fix https://github.com/dhall-lang/dhall-lang/issues/250 in version 4.0.0 of the standard was that a record of types is now treated as a kind. This is relevant to the error you got.

The standard also separately specifies that a record can store Kinds like this:

{ x = Type }

... but does not enable support for storing more general (lower-case "k") kinds, for reasons having to do with how it would be encoded in CCω.

So the exact issue here is that this:

< Private : {} | Public : {} >

... is a type, and therefore this:

{ Scopes = < Private : {} | Public : {} > }

... is a kind, but it is not a Kind, therefore you cannot store it inside of another record.

This implies that a types record cannot be nested.

[jneira]

Great explanation, as always. I feel that nesting records should be allowed in general (seems to me that it is more uniform) but i know that it is more important make sound the type system

[phadej]

Pairs

Let's start with a variant of Gabriel's example:

-- let RecordT = {x : Type, y : Type -> Type} -- we cannot write this!
let Record : {x : Type, y : Type -> Type} = {x =  Bool, y = List}
in Record.y Record.x

• dhall type says Type
• dhall says List Bool
• Record : {x : Type, y : Type -> Type} : Sort

We try to understand why this is so. Standard doesn't explain (or I fail to find)
why this is so.

Church encoding

If we look at Church encoding of pairs

-- cannot write this either:
-- let RecordT = forall (r : Kind) -> (Type -> (Type -> Type) -> r) -> r
let Record = \(r : Kind) ->
             \(f :  Type -> (Type -> Type) -> r) ->
             f Bool List
in Record Type (\(x : Type) -> \(y : Type -> Type) -> y x)

• dhall type says Type
• dhall says List Bool

So I guess this is the explanation, why records are typed in this way.

Type is impredicative

For comparison, on the term level, this is not an issue, because
Type is an impredicative universe:

-- this type is ok:
let RecordT = forall (r : Type) -> (Natural -> (Natural -> Natural) -> r) -> r
let Record : RecordT
           = \(r : Type) ->
             \(f : Natural -> (Natural -> Natural) -> r) ->
             f 42 (\(n : Natural) -> n + 1)
in Record Natural (\(x : Natural) -> \(y : Natural -> Natural) -> y x)

• dhall type says Natural
• dhall says 43
• Record : RecordT : Type, not Kind!

Because of impredicativity of Type (forall (x : Type) -> (... : Type) : Type)
we can nest records of values,
but because Kind is predicative (forall (x : Kind) -> (... : Kind) : Sort`)
a types record cannot be nested.

This is unfortunate.

Why this is not a problem, say in Agda or Coq (which are predicative)?
I present one way of thinking about this:

Agda

Church encoding

Let's first encode the Church pair in Agda, for comparison
(and get familiar with syntax)

module Expr where

open import Data.Nat using (ℕ)
open import Data.Bool using (Bool)
open import Data.List using (List)

-- Agda has universes too:
Type = Set
Kind = Set₁
Sort = Set₂
-- but there are infinitely many

RecordT : Sort
RecordT = ∀ (r : Kind) → (Type → (Type → Type) → r) → r

Record : RecordT
Record r f = f Bool List

example : Type
example = Record Type λ x y → y x

Here, Dhall and Agda work similarly. (And even look very similar!)

"Built-in" Pairs

Agda has built in products (pairs), note that
RecordT₂ : Kind

module Interlude where
  open import Data.Product

  RecordT₂ : Kind -- !!!
  RecordT₂ = Type × (Type → Type)

  Record₂ : RecordT₂
  Record₂ = Bool , List

  -- Here, Agda needs a bit of help, i.e. type annotation
  example-nested₂ : (Type × Type) × ((Type → Type) × Type)
  example-nested₂ = ((ℕ → ℕ) , Bool) , (List , Bool)

And because RecordT₂ : Kind we can nest pairs or types.

  -- Here, Agda needs a bit of help, i.e. type annotation
  example₃ : (Type × Type) × ((Type → Type) × Type)
  example₃ = ((ℕ → ℕ) , Bool) , (List , Bool)

Making them ourselves

module SimplePair where
  -- Note that A × B lives in universe below than its Church Encoding!
  record _×_ {ℓ} (A : Set ℓ) (B : Set ℓ) : Set ℓ where
    constructor _,_
    field
      proj₁ : A
      proj₂ : B

  open _×_

  RecordT₃ : Kind -- !!!
  RecordT₃ = Type × (Type → Type)

  Record₃ : RecordT₃
  Record₃ = Bool , List

  -- C-n example₂ --> List Bool
  example₃ = (proj₂ Record₃) (proj₁ Record₃)

  -- because this pair is simpler, Agda can figure out types:
  example-nested₃ = ((ℕ → ℕ) , Bool) , (List , Bool)

So, for me, it looks safe to start treating records in this way; i.e.
with "built-in" typing rules, and not "merely a syntax" for Church encoding
(I'm not sure this is the case now, it looks like it is).

Σ-types work this way (CCω paper calls them negative pairs):

 Γ ⊢ A : □ i    Γ, x : A ⊢ B : □ j
-----------------------------------
 Γ ⊢ Σ x : A, B : □ (max i j)

Note that (dependent) pair lives in □ (max i j); not the □ (succ (max i j)) !

Dhall can have very simple variant:

 Γ ⊢ A : □ i    Γ ⊢ B : □ i
----------------------------
 Γ ⊢ A × B : □ i

Or it can make having types and terms in the same pair via

 Γ ⊢ A : □ i    Γ ⊢ B : □ j
----------------------------
 Γ ⊢ A × B : □ (max i j)

The record construction is universe polymorphic already, as it works for Type
and Kind; I don't see (theoretical) reason for it not to be a bit more
polymorphic. But in practive Non-recursive right-biased merge will be
quite tricky to type (disjoint merge would be simpler). Maybe one can make
it work by requiring that overlapping fields have the same sort.

{ a = Bool } // {a = Natural} ---> { a = Natural }
{ a = Bool } // {a = List}    ---> { a = List }
{ a = Bool}  // {a = 42}      ---> error, Bool : Type : Kind; but 42 : Natural : Type; Kind /= Type

This doesn't look much different than the way Recursive record merge
requiring colliding fields are records.

TL;DR

Records (pairs is disguise) should be built-in.