Comments (17)
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
from dhall-haskell.
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 }
from dhall-haskell.
@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
from dhall-haskell.
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
from dhall-haskell.
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?
from dhall-haskell.
@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)
from dhall-haskell.
@timbod7: I also introduced a fix to prevent this sort of bad error message in dc1773f . See the commit message for more details
After that commit your original code should work
from dhall-haskell.
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.
from dhall-haskell.
Actually, I'm thinking of just banning parentheses and/or other special characters from paths/URLs
from dhall-haskell.
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.
from dhall-haskell.
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
from dhall-haskell.
I put up a pull request to increase the set of disallowed characters from paths here: #58
from dhall-haskell.
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.
from dhall-haskell.
@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
from dhall-haskell.
Why not just use the Calculus of Constructions instead of System F? Both are strongly normalizing, but CoC supports type synonyms and other goodies.
from dhall-haskell.
@ChristopherKing42: I don't believe that the calculus of constructions supports type synonyms. The limitation I described was also an issue with morte
from dhall-haskell.
@Gabriel439 Oh, that's correct (as witnessed by the morte
expression (\(id:□) -> (\(x:id)->x)(\(t:*) -> t)) (∀(t:*) -> *)
).
from dhall-haskell.
Related Issues (20)
- Failure to Decode Expression with extended Builtin Function HOT 1
- Document the significance of `Nothing :: Maybe CharacterSet`
- Please report symlink contents for `Error: Missing file` HOT 2
- Error generating docs
- combine `let` bindings in `dhall format` HOT 1
- Support request for `aeson` 2.2 in `dhall` HOT 2
- dhall-to-yaml does not properly quote strings HOT 1
- Can not install dhall-lsp-server HOT 2
- Allow hnix 0.17
- Hackage build failed for dhall-toml-1.0.3
- Get back into Stackage Nightly with GHC 9.8 HOT 1
- Missing binaries in release HOT 1
- Hackage release for dhall-lsp-server HOT 1
- Build failure on GHC 9.8.1: 'Illegal invisible type variable binder'
- Report imports HOT 1
- dhall-docs: Prelude.head: empty list
- Suggesting a new construct for dealing with optional fields in Dhall defaults
- dhall-json bound on aeson can be relaxed
- Questions regarding the right strategy for upgrading to ghc-9.8
- Build failure on macos-latest stack.yaml HOT 3
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from dhall-haskell.