-
Notifications
You must be signed in to change notification settings - Fork 211
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
The new union access is not transitive across record field #692
Comments
Well. it seems this was already discussed in the pr. So, would be an alternative to |
Adding a let with the record field makes it work too:
I feel that behaviour it is not very intuitive 🤔 |
@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. |
Fixes #692 The standard permits a user to access a constructor from a type stored inside a record, but the Haskell implementation had a mistake which prevented this. Specifically, the Haskell implementation was not normalizing the union type as the standard specified before attempting to access the constructor, leading to an unexpected type error.
Fix is up here: #694 I will merge that before cutting the release tonight if nobody objects |
Fixes #692 The standard permits a user to access a constructor from a type stored inside a record, but the Haskell implementation had a mistake which prevented this. Specifically, the Haskell implementation was not normalizing the union type as the standard specified before attempting to access the constructor, leading to an unexpected type error.
Just tested with
fails with
explained:
This one follows the new dhall spec? |
Yep, that's correct - you can no longer have mixed records.
…On Thu, 22 Nov 2018, 7:24 am Javier Neira ***@***.*** 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
<#692 (comment)>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/AABRjgyKsl1FdNXZhFOMcDQYRPQd8Tc0ks5uxlESgaJpZM4YsxCD>
.
|
Actually, it's disallowed for a different reason. To explain why, I'll need to specify some terminology:
All
Carefully note that in version 3.0.0 of the standard a record of types was treated as a type instead of a kind:
One of the necessary changes to fix dhall-lang/dhall-lang#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
... 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:
... is a type, and therefore this:
... is a kind, but it is not a This implies that a types record cannot be nested. |
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 |
PairsLet'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
We try to understand why this is so. Standard doesn't explain (or I fail to find) Church encodingIf 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)
So I guess this is the explanation, why records are typed in this way. Type is impredicativeFor comparison, on the term level, this is not an issue, because -- 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)
Because of impredicativity of This is unfortunate. Why this is not a problem, say in Agda or Coq (which are predicative)? AgdaChurch encodingLet's first encode the Church pair in Agda, for comparison 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" PairsAgda has built in products (pairs), note that 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 -- Here, Agda needs a bit of help, i.e. type annotation
example₃ : (Type × Type) × ((Type → Type) × Type)
example₃ = ((ℕ → ℕ) , Bool) , (List , Bool) Making them ourselvesmodule 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. Σ-types work this way (CCω paper calls them negative pairs):
Note that (dependent) pair lives in Dhall can have very simple variant:
Or it can make having types and terms in the same pair via
The record construction is universe polymorphic already, as it works for
This doesn't look much different than the way Recursive record merge TL;DRRecords (pairs is disguise) should be built-in. |
Fixes dhall-lang/dhall-haskell#692 The motivation for this change is to permit nested records of types. This changes a record of types to be treated as a type instead of a kind, as suggested by @phadej in dhall-lang/dhall-haskell#692 (comment) The original encoding of a record of types used kind polymorphism, which meant that a record of types behaved like a kind instead of a type. However, there's another way to encode records which takes advantage of the fact that they have a finite number of fields of of known type by desugaring them to a finite number of function arguments. In other words, a function of this type: ```haskell ∀(r : { x : Type, y : Type → Type }) → … ``` ... desugars to a function of this type: ```haskell ∀(x : Type) → ∀(y : Type → Type) → … ``` Similarly, the following anonymouse function: ```haskell ∀(r : { x : Type, y : Type → Type }) → … ``` ... desugars to: ```haskell λ(x : Type) → λ(y : Type → Type) → … ``` Accessing a field from an abstract record: ```haskell ∀(r : { x : Type, y : Type → Type }) → … r.x … ``` ... translates to referencing the correct parameter: ```haskell λ(x : Type) → λ(y : Type → Type) → … x … ``` Function application where the record is an argument: ```haskell f { x = Bool, y = List } -- or: ∀(r : { x : Type, y : Type → Type }) → … f r … ``` ... desugars to applying the function to each field: ```haskell f Bool List -- or: λ(x : Type) → λ(y : Type → Type) → … f x y … ``` If you encode things this way then a record of types behaves like a type. To be precise, a record is a valid function argument if and only if its constituent fields are also valid function arguments, so if its fields are types then you can treat a record of them as a type, too.
... as standardized in dhall-lang/dhall-lang#300 Fixes #692
Fixes dhall-lang/dhall-haskell#692 The motivation for this change is to permit nested records of types. This changes a record of types to be treated as a type instead of a kind, as suggested by @phadej in dhall-lang/dhall-haskell#692 (comment) The original encoding of a record of types used kind polymorphism, which meant that a record of types behaved like a kind instead of a type. However, there's another way to encode records which takes advantage of the fact that they have a finite number of fields of of known type by desugaring them to a finite number of function arguments. In other words, a function of this type: ```haskell ∀(r : { x : Type, y : Type → Type }) → … ``` ... desugars to a function of this type: ```haskell ∀(x : Type) → ∀(y : Type → Type) → … ``` Similarly, the following anonymouse function: ```haskell ∀(r : { x : Type, y : Type → Type }) → … ``` ... desugars to: ```haskell λ(x : Type) → λ(y : Type → Type) → … ``` Accessing a field from an abstract record: ```haskell ∀(r : { x : Type, y : Type → Type }) → … r.x … ``` ... translates to referencing the correct parameter: ```haskell λ(x : Type) → λ(y : Type → Type) → … x … ``` Function application where the record is an argument: ```haskell f { x = Bool, y = List } -- or: ∀(r : { x : Type, y : Type → Type }) → … f r … ``` ... desugars to applying the function to each field: ```haskell f Bool List -- or: λ(x : Type) → λ(y : Type → Type) → … f x y … ``` If you encode things this way then a record of types behaves like a type. To be precise, a record is a valid function argument if and only if its constituent fields are also valid function arguments, so if its fields are types then you can treat a record of them as a type, too.
... as standardized in dhall-lang/dhall-lang#300 Fixes #692
This dhall definition works as intended:
However, puting the union in a record field doesnt work (at least as i expected):
It throws:
The text was updated successfully, but these errors were encountered: