Skip to content
Permalink
Browse files

Add support for dependent types (#669)

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.
  • Loading branch information...
Gabriel439 committed Aug 4, 2019
1 parent 9f259cd commit 1ed98c33ce5078161109885f0b16b3828958f4e2
Showing 386 changed files with 1,523 additions and 1,475 deletions.
@@ -1,18 +1,14 @@
{-
The `and` function returns `False` if there are any `False` elements in the
`List` and returns `True` otherwise
Examples:
```
./and [ True, False, True ] = False
./and ([] : List Bool) = True
```
-}
let and
: List Bool Bool
= λ(xs : List Bool)
List/fold Bool xs Bool (λ(l : Bool) λ(r : Bool) l && r) True

let example0 = assert : and [ True, False, True ] False

let example1 = assert : and ([] : List Bool) True

in and
@@ -1,17 +1,18 @@
{-
`build` is the inverse of `fold`
Examples:
```
./build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → true) = True
./build (λ(bool : Type) → λ(true : bool) → λ(false : bool) → false) = False
```
-}
let build
: ((bool : Type) (true : bool) (false : bool) bool) Bool
= λ(f : (bool : Type) (true : bool) (false : bool) bool)
f Bool True False

let example0 =
assert
: build (λ(bool : Type) λ(true : bool) λ(false : bool) true) True

let example1 =
assert
: build (λ(bool : Type) λ(true : bool) λ(false : bool) false)
False

in build
@@ -1,22 +1,18 @@
{-
Returns `True` if there are an even number of `False` elements in the list and
returns `False` otherwise
Examples:
```
./even [ False, True, False ] = True
./even [ False, True ] = False
./even [ False ] = False
./even ([] : List Bool) = True
```
-}
let even
: List Bool Bool
= λ(xs : List Bool)
List/fold Bool xs Bool (λ(x : Bool) λ(y : Bool) x == y) True

let example0 = assert : even [ False, True, False ] True

let example1 = assert : even [ False, True ] False

let example2 = assert : even [ False ] False

let example3 = assert : even ([] : List Bool) True

in even
@@ -1,13 +1,5 @@
{-
`fold` is essentially the same as `if`/`then`/else` except as a function
Examples:
```
./fold True Natural 0 1 = 0
./fold False Natural 0 1 = 1
```
-}
let fold
: (b : Bool) (bool : Type) (true : bool) (false : bool) bool
@@ -17,4 +9,8 @@ let fold
λ(false : bool)
if b then true else false

let example0 = assert : fold True Natural 0 1 0

let example1 = assert : fold False Natural 0 1 1

in fold
@@ -1,12 +1,10 @@
{-
Flip the value of a `Bool`
-}
let not : Bool Bool = λ(b : Bool) b == False

Examples:
let example0 = assert : not True False

```
./not True = False
let example1 = assert : not False True

./not False = True
```
-}
let not : Bool Bool = λ(b : Bool) b == False in not
in not
@@ -1,22 +1,18 @@
{-
Returns `True` if there are an odd number of `True` elements in the list and
returns `False` otherwise
Examples:
```
./odd [ True, False, True ] = False
./odd [ True, False ] = True
./odd [ True ] = True
./odd ([] : List Bool) = False
```
-}
let odd
: List Bool Bool
= λ(xs : List Bool)
List/fold Bool xs Bool (λ(x : Bool) λ(y : Bool) x != y) False

let example0 = assert : odd [ True, False, True ] False

let example1 = assert : odd [ True, False ] True

let example2 = assert : odd [ True ] True

let example3 = assert : odd ([] : List Bool) False

in odd
@@ -1,18 +1,14 @@
{-
The `or` function returns `True` if there are any `True` elements in the `List`
and returns `False` otherwise
Examples:
```
./or [ True, False, True ] = True
./or ([] : List Bool) = False
```
-}
let or
: List Bool Bool
= λ(xs : List Bool)
List/fold Bool xs Bool (λ(l : Bool) λ(r : Bool) l || r) False

let example0 = assert : or [ True, False, True ] True

let example1 = assert : or ([] : List Bool) False

in or
@@ -1,13 +1,11 @@
{-
Render a `Bool` as `Text` using the same representation as Dhall source code
(i.e. beginning with a capital letter)
-}
let show : Bool Text = λ(b : Bool) if b then "True" else "False"

Examples:
let example0 = assert : show True "True"

```
./show True = "True"
let example1 = assert : show False "False"

./show False = "False"
```
-}
let show : Bool Text = λ(b : Bool) if b then "True" else "False" in show
in show
@@ -1,13 +1,11 @@
{-
Render a `Double` as `Text` using the same representation as Dhall source
code (i.e. a decimal floating point number with a leading `-` sign if negative)
-}
let show : Double Text = Double/show

Examples:
let example0 = assert : show -3.1 "-3.1"

```
./show -3.1 = "-3.1"
let example1 = assert : show 0.4 "0.4"

./show 0.4 = "0.4"
```
-}
let show : Double Text = Double/show in show
in show
@@ -1,12 +1,5 @@
{-
Compose two functions into one.
Examples:
```
./compose Natural Natural Bool (λ(n : Natural) → n + n) ../Natural/even 3
= True
```
-}
let compose
: (a : Type) (b : Type) (c : Type) (a b) (b c) a c
@@ -18,4 +11,9 @@ let compose
λ(x : A)
g (f x)

let example0 =
assert
: compose Natural Natural Bool (λ(n : Natural) n + n) Natural/even 3
True

in compose
@@ -2,13 +2,11 @@
Render an `Integer` as `Text` using the same representation as Dhall source
code (i.e. a decimal number with a leading `-` sign if negative and a leading
`+` sign if non-negative)
-}
let show : Integer Text = Integer/show

Examples:
let example0 = assert : show -3 "-3"

```
./show -3 = "-3"
let example1 = assert : show +0 "+0"

./show +0 = "+0"
```
-}
let show : Integer Text = Integer/show in show
in show
@@ -1,12 +1,10 @@
{-
Convert an `Integer` to the corresponding `Double`
-}
let toDouble : Integer Double = Integer/toDouble

Examples:
let example0 = assert : toDouble -3 -3.0

```
./toDouble -3 = -3.0
let example1 = assert : toDouble +2 2.0

./toDouble +2 = 2.0
```
-}
let toDouble : Integer Double = Integer/toDouble in toDouble
in toDouble
@@ -1,17 +1,14 @@
{-
Builds a key-value record such that a List of them will be converted to a
homogeneous record by dhall-to-json and dhall-to-yaml.
Both key and value are fixed to Text.
Take a look at `Record/keyValue` for a polymorphic version.
Example:
```
./keyText "foo" "bar" = { mapKey = "foo", mapValue = "bar" }
```
-}

let keyText =
λ(key : Text) λ(value : Text) { mapKey = key, mapValue = value }

let example0 =
assert : keyText "foo" "bar" { mapKey = "foo", mapValue = "bar" }

in keyText
@@ -1,20 +1,17 @@
{-
Builds a key-value record such that a List of them will be converted to a
homogeneous record by dhall-to-json and dhall-to-yaml.
Examples:
```
./keyValue Natural "foo" 2 = { mapKey = "foo", mapValue = 2 }
./keyValue Text "bar" "baz" = { mapKey = "bar", mapValue = "baz" }
```
-}

let keyValue =
λ(v : Type)
λ(key : Text)
λ(value : v)
{ mapKey = key, mapValue = value }

let example0 =
assert : keyValue Natural "foo" 2 { mapKey = "foo", mapValue = 2 }

let example1 =
assert : keyValue Text "bar" "baz" { mapKey = "bar", mapValue = "baz" }

in keyValue
@@ -45,13 +45,13 @@ let object
}
)
json.object
( List/map
{ mapKey : Text, mapValue : JSON@1 }
{ mapKey : Text, mapValue : JSON }
( λ(kv : { mapKey : Text, mapValue : JSON@1 })
{ mapKey = kv.mapKey, mapValue = kv.mapValue JSON json }
( List/map
{ mapKey : Text, mapValue : JSON@1 }
{ mapKey : Text, mapValue : JSON }
( λ(kv : { mapKey : Text, mapValue : JSON@1 })
{ mapKey = kv.mapKey, mapValue = kv.mapValue JSON json }
)
x
)
x
)

in object

0 comments on commit 1ed98c3

Please sign in to comment.
You can’t perform that action at this time.