Literal / singleton types, or value level restrictions

#1

Hello, I am trying to figure out if dhall can limit/restrict/validate values

Let me illustrate with and example

Having a file test.yaml

someflag: true

yaml-to-dhall 'let OnlyTrue = < true > in { someflag : OnlyTrue }' --file ./test.yaml


Error: Dhall type expression and YAML value do not match:

Expected Dhall type:
< true >

YAML:
true

I would expect the above to succeed.
And it to fail for someflag: false

I believe it’s called literal types
https://www.typescriptlang.org/v2/docs/handbook/literal-types.html#string-literal-types

I am sort of looking for the oposite to https://prelude.dhall-lang.org/v11.1.0/JSON/package.dhall

where i would define a
a let OnlyTrue/fromJson = ...

#2

@fkowal: That cannot currently be specified at the type level, but since Dhall has nascent support for dependent types we might be able to add support for that in some way.

One solution that doesn’t require any language changes might be to add support for this just to yaml-to-dhall. In other words, define a Prelude.JSON.Where : (JSON -> Bool) -> Type dependent type that yaml-to-dhall recognizes that you could use like this:

let isTrue : JSON -> Bool = …

in  { someflag : Where isTrue }
#3

Technically, such “literal types” work already by Church-encoded equality and existentials:

let Eq : forall (A : Type) -> A -> A -> Type
  = \(A : Type) -> \(a : A) -> \(b : A) ->
     (forall (P : A -> Type) -> P a -> P b)

let refl : forall (A : Type) -> forall (a : A) -> Eq A a a
  = \(A : Type) -> \(a : A) -> \(P : A -> Type) -> \(pa : P a) -> pa

let exists =
  \(A : Type) -> \(B : A -> Type) ->
     forall (C : Type)
  -> forall (f : forall (a : A) -> B a -> C)
  -> C

-- pack : {A B} → (a : A) → B a → exists A B
let pack = \(A : Type) -> \(B : A -> Type) -> \(a : A) -> \(ba : B a) ->
           \(C : Type) -> \(f : forall (a : A) -> B a -> C) ->
		   f a ba

-- generically, the type of Bool-s which are true is the following:
let OnlyTrue = exists Bool (\(b : Bool) -> Eq Bool b True)

-- obviously verbose as hell
let myTrue : OnlyTrue
  = pack Bool (\(b : Bool) -> Eq Bool b True) True (refl Bool True)

in myTrue

But I find this too verbose to be usable.

#4

The original request also reminded of this issue:

#5

@AndrasKovacs: You can simplify that a little bit by using the existing language support for REFL (assert) and equality (≡):

let exists
    : ∀(A : Type) → (A → Type) → Type
    =   λ(A : Type)
      → λ(B : A → Type)
      → ∀(C : Type) → ∀(f : ∀(a : A) → B a → C) → C

let pack
    : ∀(A : Type) → ∀(B : A → Type) → ∀(a : A) → B a → exists A B
    =   λ(A : Type)
      → λ(B : A → Type)
      → λ(a : A)
      → λ(ba : B a)
      → λ(C : Type)
      → λ(f : ∀(a : A) → B a → C)
      → f a ba

let OnlyTrue = exists Bool (λ(b : Bool) → b ≡ True)

let myTrue
    : OnlyTrue
    = pack Bool (λ(b : Bool) → b ≡ True) True (assert : True ≡ True)

in  myTrue
#6

@AndrasKovacs: So I’m trying to think if this can be turned into an ergonomic language feature. The rough idea I have in mind is that we could support for existentially quantified types that might be used like this:

let myTrue
      : ∃(b : Bool) → b ≡ True
      = pack True (assert : True ≡ True)

let bool0
      : Bool
      = merge
        { pack = λ(b : Bool) → λ(_ : b ≡ True) → b }
        myTrue

let bool1
      : Bool
      = unpack myTrue

In other words:

  • Add a new ∃/exists type former
  • Add a pack keyword to constructor a value of that type
  • Provide a way to “pattern match” on a pack for the general case
  • Provide an unpack keyword to extract the existentially quantified value as a convenience

… and to tie this back to the original request, we could add YAML/JSON tooling support for existentially quantified values

#7

Sigma types would be better than existentials. I only used the latter because sigmas cannot be emulated with Church-encoding. For sigmas dependent record types a la Agda (but generically as in Dhall, instead of nominally) would be an ergonomic solution. From the perspective of having a nice core language, it would be best to only have dependent record types, and non-dependent records would be a special case. However, that requires

  • significant change in record behavior and operations; e.g. fields must be ordered and record type/value concatenation must be generalized to the dependent case
  • bidirectional checking, because dependent records are checkable but very rarely inferable. For inference one can default to the non-dependent case, but we’d still want checking so that dependent records are usable.
2 Likes
#8

Just to note: we talked about dependent sums before in the context of implementing Vector types. If we are thinking of standardising dependent sums, probably good to collect use cases together.

#9

@AndrasKovacs: I think it would be fine to have two separate record types (one dependent and one non-dependent). Syntactically it would not be an issue because we could use, say, {{…}} to distinguish a dependent record literal / type. One reason I hadn’t done so already is that we just didn’t yet have a compelling use case and I was trying to keep the language simple.

So, my understanding is that if we had such a type, then we could write:

let myTrue
      : {{ value : Bool, constraint : value ≡ True }}
      = {{ value = True, constraint = assert : True ≡ True }}

… and then we would need to provide some sort of dependent elimination (possibly using the merge keyword as before) and optionally support for accessing the first field of the record (e.g. myTrue.value) as a convenience.

#10

Dependent elimination is not needed, only field projections. Elimination is derivable from projections and beta-eta rules.

I stress though that no matter how they are implemented, dependent records really need bidirectional checking. Without that, the only way to infer type for a dependent record literal is to always directly annotate it with its type. Hence, the following would work:

{{ value = True, constraint = assert : True ≡ True }} : {{ value : Bool, constraint : value ≡ True }}

But the following would only work bidirectionally:

let f : Text -> {{ value : Bool, constraint : value ≡ True }}
  = \(t : Text) -> {{ value = True, constraint = assert : True ≡ True}}
2 Likes