Skip to content
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

Add support for dependent types #669

Merged
merged 9 commits into from Aug 4, 2019

Conversation

@Gabriel439
Copy link
Contributor

commented Jul 28, 2019

The immediate motivation for this change is to add language support for
assertions verified at type-checking time, like this:

let isZero : Natural  Bool = Natural/isZero

let example0 = assert : isZero 2  False

let example1 = assert : isZero 0  True

in isZero

Now all the examples in the Prelude no longer need to be comments, so we
can remove them from the test suite and check those examples directly
within the code.

This would allow users to add tests to Dhall code. A unit test would be
like the above example comparing literal values. A "property test" in
Dhall would actually be verified via symbolic reasoning, like this:

λ(n : Natural)  assert : n  (n + 0)

The biggest disadvantage of this change is that we will need to spend
more time on improving the robustness of our judgmental equality check
if users really want to take advantage of Dhall's symbolic reasoning.
In the worst case, though, we can just say no to robust symbolic
reasoning and commit to only supporting unit tests in the short term.

Add support for dependent types
The immediate motivation for this change is to add language support for
assertions verified at type-checking time, like this:

```dhall
let isZero : Natural → Bool = Natural/isZero

let example0 = assert : isZero 2 ≡ False

let example1 = assert : isZero 0 ≡ False

in isZero
```

Now all the examples in the Prelude no longer need to be comments, so we
can remove them from the test suite and check those examples directly
within the code.

This would allow users to add tests to Dhall code.  A unit test would be
like the above example comparing literal values.  A "property test" in
Dhall would actually be verified via symbolic reasoning, like this:

```dhall
λ(n : Natural) → assert : n ≡ (n + 0)
```

The biggest disadvantage of this change is that we will need to spend
more time on improving the robustness of our judgmental equality check
if users really want to take advantage of Dhall's symbolic reasoning.
In the worst case, though, we can just say no to robust symbolic
reasoning and commit to only supporting unit tests in the short term.

Gabriel439 added a commit to dhall-lang/dhall-haskell that referenced this pull request Jul 28, 2019

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

commented Jul 28, 2019

Here's the matching change to the Haskell implementation:

Note that the Prelude lint will fail until I update it to use the Haskell implementation

Also, sorry for the large diff! Most of it is just noise from changing all the Prelude files to take advantage of the new support for unit tests. The actual changes to the standard are quite small.

@philandstuff
Copy link
Collaborator

left a comment

Looks great! Two minor comments on the ABNF.

standard/dhall.abnf Outdated Show resolved Hide resolved
standard/dhall.abnf Outdated Show resolved Hide resolved
@ocharles

This comment has been minimized.

Copy link
Member

commented Jul 28, 2019

Is there any reason why assert has to be annotated and can't just take a type as a function argument? That is, could we have assert ( a === b ) instead?

@f-f

This comment has been minimized.

Copy link
Member

commented Jul 28, 2019

This is cool 👏🎉

I'll take a look at the diff later, but I just realized that this allows "text equality at compile time" (which is good by me, just noting it so we're aware of what it entails)

I.e. this will typecheck:

let a = "foo" in assert : a === "foo"

..but this doesn't:

let a = "foo" in assert : a === "bar"

..nor this one (i.e. one cannot extract it into an import and feed it arbitrary text):

λ( x : Text )  assert : x === "foo"

In the end this might be striking the right balance between "no text equality at all" and "full text equality on any text"

@Nadrieril

This comment has been minimized.

Copy link
Collaborator

commented Jul 28, 2019

@Gabriel439 So you think you could make a separate commit to update the tests, so that we can see the standard changes more easily ?

@singpolyma

This comment has been minimized.

Copy link
Collaborator

commented Jul 28, 2019

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

commented Jul 28, 2019

@Nadrieril: You can filter the diff by file type using the "File filter..." drop-down, so if you filter to just .md it will narrow things down to just the standard-related changes

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

commented Jul 28, 2019

@ocharles: Like most cases where the grammar uses a type annotation, it's to leave the door open for a smoother transition to type inference later on. It also the same number of characters.

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

commented Jul 28, 2019

@f-f: Yes, in my opinion equality checking of Text at type-checking time is okay because Dhall can detect and flag the error. Contrast that with a normalization-time Text comparison that returns False or a None, where Dhall thinks nothing is wrong because the result is well-typed, which pushes error-handling downstream.

Also, as you noted, it can't really be used to implement to check preconditions or any dynamic program values: it can really only be used for unit tests and "property tests" (symbolic reasoning)

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

commented Jul 29, 2019

@singpolyma: Oops! Yeah, you're right. Something in the test suite needs to still refer to the Prelude files, even if just to trivially import them

@Profpatsch

This comment has been minimized.

Copy link
Member

commented Jul 29, 2019

let isZero : Natural → Bool = Natural/isZero

let example0 = assert : isZero 2 ≡ False

let example1 = assert : isZero 0 ≡ True

in isZero

What strikes me in this example is that example0 and example1 are not actually used anywhere. Does this mean that dhall can never get support for ignoring unused types in its typechecking phase?

@ocharles

This comment has been minimized.

Copy link
Member

commented Jul 29, 2019

What strikes me in this example is that example0 and example1 are not actually used anywhere.

Also, won't dhall lint just delete these? Never mind, I see it's been coded to avoid them.

Ultimately I'm not huge on this level of magic. I'd much prefer assert T x to normalize to x but check that T type checks.

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

commented Jul 30, 2019

@Profpatsch: That is already the case currently. If you write let unused : Text = 1 in 2 that is a type error and I think it makes sense to keep it that way

To illustrate why, consider this equivalent expression:

(λ(unused : Text)  2) 1

If we ignored type errors for unused variables in let expressions then for consistency we'd also have to sometimes ignore type mismatch errors for function application, which doesn't sit right with me.

@Nadrieril

This comment has been minimized.

Copy link
Collaborator

commented Jul 30, 2019

@ocharles If we go your way, I expect that a lot of people would write let unused = assert (a === b) 0 in ... to avoid having asserts littering actual code, so I'm not sure it's really less magical.
Doing it as proposed means we also get access to terms of type a === b, which could be useful in the future if we allow manipulating those things to create more complex proofs manually.

Gabriel439 added some commits Aug 1, 2019

Exercise Prelude
... as caught by @singpolyma

This is now as simple as just importing `./package.dhall`,
which transitively imports all of the assertions
@Nadrieril

This comment has been minimized.

Copy link
Collaborator

commented Aug 1, 2019

Shouldn't the big Prelude test be in typecheck instead of normalization ?

-}
let build
: ((bool : Type) (true : bool) (false : bool) bool) Bool
= λ(f : (bool : Type) (true : bool) (false : bool) bool)
f Bool True False

let example0 =

This comment has been minimized.

Copy link
@singpolyma

singpolyma Aug 1, 2019

Collaborator

This is fine, but would examples = [ assert ..., assert ... ] be cleaner?

This comment has been minimized.

Copy link
@Gabriel439

Gabriel439 Aug 2, 2019

Author Contributor

Each assertion has a different type, so they can't be stored within the same list

For example, in this file the fully normalized types of the examples are:

example0 : True  True

example1 : False  False
@singpolyma

This comment has been minimized.

Copy link
Collaborator

commented Aug 1, 2019

So, AFAICT the === operator is basically meaningless unless directly fed into an assert? Am I reading that right?

@Nadrieril

This comment has been minimized.

Copy link
Collaborator

commented Aug 1, 2019

@singpolyma Essentially yes. If I'm not mistaken, A === B is a special type that has exactly one inhabitant if A and B are equivalent, and no inhabitants otherwise. The only inhabitant is assert. assert is often called Refl in other contexts.
In the future, we could have other uses for this type, but for now it's only useful to use it with assert.

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

commented Aug 2, 2019

@Nadrieril: Oops, you're right. I'll move the Prelude test to the appropriate location

@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

commented Aug 2, 2019

Also, to learn more about what @Nadrieril is referring to, I recommend reading up on how Agda does this:

https://plfa.github.io/Equality/

... because this proposal is inspired by the Agda model for propositional equality.

In fact, Dhall steals a lot of things from Agda and this no exception. To a first approximation, Dhall is the "Agda of configuration languages".

Fix precedence of `assert`
... as caught via discussion with @philandstuff
@Gabriel439

This comment has been minimized.

Copy link
Contributor Author

commented Aug 3, 2019

Alright, I think I've addressed everybody's feedback. If nobody has any objections then I plan to merge tomorrow (after sorting out the CI failures)

Gabriel439 added some commits Aug 4, 2019

Update `dhall` version
... so that `lint-prelude` accepts the test files

@Gabriel439 Gabriel439 merged commit 1ed98c3 into master Aug 4, 2019

1 check passed

hydra Hydra build #26654 of dhall-lang:669:dhall-lang
Details

@Gabriel439 Gabriel439 deleted the gabriel/dependent_types branch Aug 4, 2019

ocharles added a commit that referenced this pull request Aug 7, 2019

Restore the CI check for `dhall lint` (#679)
This was accidentally changed to `dhall format` in #669
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
7 participants
You can’t perform that action at this time.