Dhall-haskell: Type annotation cannot refer bindings in scope

[esmolanka]

In "fixed" example from #9 different kind of error occurs to the user. The type checker cannot determine that {x : Integer, y : Integer} == Point.

$ ./dhall <<< "let Point = {x : Integer, y : Integer} in ({x = 42, y = -1} : Point)"

Use "dhall --explain" for detailed errors

Point : Type

Error: Expression doesn't match annotation

({x = 42, y = -1} : Point)

(stdin):1:43

Being able to declare type aliases and then use them in type annotations is especially useful when it comes to List or Optional type, because literals of such types always require type annotations. Duplicating type of large record does not seem practical.

[Gabriel439]

So this is actually intended behavior, surprising as that may be.

Short explanation

Type-checking precedes normalization and normalization includes substitution of let-bound types

Recommended solution

You can use the import system to solve this problem:

$ echo "{ x : Integer, y : Integer }" > ./Point
$ dhall <<< "{x = 42, y = -1} : ./Point"
{ x : Integer, y : Integer }

{ x = 42, y = -1 }

Long explanation

Dhall has a rule that:

let x : t = y in e

... must be equivalent to this

(λ(x : t) → e) y

... both for normalization purposes and type-checking purposes. That means that:

• Both expressions should normalize to the same result
• If one expression type-checks then the other expression must type-check
• If one expression fails to type-check then the other expression must fail to type-check

That means that this let expression

let Point : Type = {x : Integer, y : Integer} in ({x = 42, y = -1} : Point)

... must behave the same as this equivalent λ expression:

(λ(Point : Type) → ({ x = 42, y = -1 } : Point)) { x : Integer, y : Integer }

... which does not type-check in System Fω (the type system that Dhall is based on), because this sub-expression does not type-check in isolation:

λ(Point : Type) → ({ x = 42, y = -1 } : Point)

You can try to type-check either of those expressions in Dhall and you will get the same result:

$ dhall
(λ(Point : Type) → ({ x = 42, y = -1 } : Point)) { x : Integer, y : Integer }
^D
Use "dhall --explain" for detailed errors

Point : Type

Error: Expression doesn't match annotation

({ x = 42, y = -1 } : Point)

(stdin):1:20

System Fω provides no mechanism for something equivalent to Haskell's type synonyms, for the same reason I mentioned above: type-checking precedes substitution/normalization.

You might think: "Why not provide an additional normalization step for just substituting types that precedes type-checking?"

Well, that has issues of its own. For example, how would we deal with this:

    let makeType = λ(t : Type) → { x : Integer, y : t }
in  let Point = makeType Integer
in  { x = 42, y = -1 } : Point

If we add an additional normalization step just for types then we also need another type-checking step to ensure that type formers like makeType Integer are well formed. Otherwise, the user could introduce a type error at the type formation stage like this:

    let makeType = λ(t : Type) → { x : Integer, y : t }
in  let Point = makeType 1  -- Type error
in  { x = 42, y = -1 } : Point

However, Dhall does provide an additional feature that System Fω does not, which is the import system. Since imports precede type-checking you can use them to simplify types as mentioned in the above "Work-around" section

[timbod7]

I'm trying to understand the right way to name types (to avoid duplication).

This works as I expect:

let p
  = { name = "Joe", age = +37, address = "somewhere" }
in  
let older
  = \(person : { name : Text, age : Natural, address : Text })
  ->  { name=person.name, age=person.age + +10, address=person.address}
in  

older p

giving

{ address : Text, age : Natural, name : Text }

{ address = "somewhere", age = +47, name = "Joe" }

And from the earlier comments in this thread, I see that assuming

$ cat Person 
{ name : Text, age : Natural, address : Text }

this works also:

let p
  = { name = "Joe", age = +37, address = "somewhere" } : ./Person
in  
let older
  = \(person : { name : Text, age : Natural, address : Text })
  ->  { name=person.name, age=person.age + +10, address=person.address}
in  

older p

But this doesn't:

let p
  = { name = "Joe", age = +37, address = "somewhere" } : ./Person
in  
let older
  = \(person : ./Person)
  ->  { name=person.name, age=person.age + +10, address=person.address}
in  

older p

giving:

stdin):7:1: error: expected: "''",
    "(", ")", "+", "-", ".", ":",
    built-in value, double, import,
    integer, label, list literal,
    natural, operator,
    record literal, record type,
    string, union literal,
    union type
in   
^    

Am I missing something obvious?

[Gabriel439]

@timbod7: You need to put a space in between ./Person and ) on line 5, like this:

let p
  = { name = "Joe", age = +37, address = "somewhere" } : ./Person
in  
let older
  = \(person : ./Person )
  ->  { name=person.name, age=person.age + +10, address=person.address}
in  

older p

This is because file paths consume all characters up to the first whitespace character (including parentheses)

[Gabriel439]

@timbod7: I also introduced a fix to prevent this sort of bad error message in dc1773f1af3949bf5cbf130d6de0ea666e56a727 . See the commit message for more details

After that commit your original code should work

[Profpatsch]

This is because file paths consume all characters up to the first whitespace character (including parentheses)

As a side note (and since I’m trying to understand parsing better): Would keeping the context of “being inside parentheses and interpreting a <link>) accordingly if it means closing that context” make the parser context-sensitive? It also sounds kind of complicated to implement in a theoretically sound general way.

[Gabriel439]

Actually, I'm thinking of just banning parentheses and/or other special characters from paths/URLs

[Profpatsch]

How about fencing paths with another set of separators, e.g. <>?

You wouldn’t need >-escaping probably, if you tokenize the path up to > + [ }):] or something like that. Maybe that would lead to even weirder parser edge cases though …

This way ./ wouldn’t be needed as well:

<Point> – the file ./Point
</foo/bar> – /foo/bar

let prelude = ipfs://…
in prelude/<List/null>

The last two lines are a questionable attempt to add namespaces.

[Gabriel439]

I'd prefer to just disallow reserved symbols from paths since it is simpler and I don't think people will want to use those symbols in paths or URLs anyway

Also, note that can almost get all the features of namespaces by importing a record:

let module = http://www.example.com
in  module.foo module.bar

The only issue with that is Dhall does not allow records to have types as fields

[Gabriel439]

I put up a pull request to increase the set of disallowed characters from paths here: https://github.com/Gabriel439/Haskell-Dhall-Library/pull/58

[Gabriel439]

I'll go ahead and close this since I've explained why Dhall does not support type synonyms and how to use imports instead to share type annotation logic

[ocharles]

I'd like to add that I just hit exactly this problem. I think it needs to be documented somewhere more visible than GitHub. For me this is actually a tad problematic as I was hoping to send Dhall expressions over the wire, so import syntax doesn't really work, unless the import is available to the remote machine. This in turn assumes that the client is able to host expressions, which in general is not true - as my client environment is just a web browser.

[Gabriel439]

@ocharles: Yeah, I can add this to FAQ section of the tutorial

I also need to know a bit more about your use case to suggest possible solutions.

For example, is the goal to let users interactively edit and submit these expressions in the browser? If so, you could use the IPFS Javascript API to save intermediate expressions to IPFS urls. This is probably a useful feature to implement regardless of whether users need it for type synonyms

Is there a large type that you expect your users to frequently use? If so, then host it on IPFS ahead of time. I have a NixOps recipe for hosting the Dhall Prelude on IPFS that you can reuse here:

https://github.com/dhall-lang/dhall-haskell/tree/master/ipfs

Are the clients mostly static programs written in Javascript? If so, they can define the expression once locally, resolve imports ahead of time (using the command-line interpreter) and then submit an import-free expression to your server

[ChristopherKing42]

Why not just use the Calculus of Constructions instead of System F? Both are strongly normalizing, but CoC supports type synonyms and other goodies.

[Gabriel439]

@ChristopherKing42: I don't believe that the calculus of constructions supports type synonyms. The limitation I described was also an issue with morte

[ChristopherKing42]

@Gabriel439 Oh, that's correct (as witnessed by the morte expression (\(id:□) -> (\(x:id)->x)(\(t:*) -> t)) (∀(t:*) -> *)).

[Gabriel439]

@ChristopherKing42: You might also want to check out this great paper by Simon Peyton Jones explaining pure type systems:

https://www.microsoft.com/en-us/research/wp-content/uploads/1997/01/henk.pdf

It explains how System F, System F-omega, and the calculus of constructions relate to one another by explaining them in terms of the more general pure type system framework

The other reason to read the paper is that Morte is basically a renamed Henk plus support for file-based imports

[Gabriel439]

I just want to update that Dhall does now support type synonyms on master. The original example now works:

$ dhall <<< "let Point = {x : Integer, y : Integer} in ({x = 42, y = -1} : Point)"
{ x : Integer, y : Integer }

{ x = 42, y = -1 }