darkkirb/dhall-nix-lib
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

switch to fixed dhall

Browse source
This commit is contained in:
Charlotte 🦝 Delenk 2022-09-07 17:01:16 +01:00
parent b110661903
commit cdf878533b
Signed by: darkkirb
GPG key ID: AB2BD8DAF2E37122
195 changed files with 21 additions and 4584 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
Bool/and.dhall
View file

@ -1,14 +0,0 @@
{-|
The `and` function returns `False` if there are any `False` elements in the
`List` and returns `True` otherwise
-}
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

16
Bool/build.dhall
View file

@ -1,16 +0,0 @@
--| `build` is the inverse of `fold`
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

20
Bool/even.dhall
View file

@ -1,20 +0,0 @@
{-|
Returns `True` if there are an even number of `False` elements in the list and
returns `False` otherwise.
This function is the `Monoid` for the `==` operation.
-}
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

14
Bool/fold.dhall
View file

@ -1,14 +0,0 @@
--| `fold` is essentially the same as `if`/`then`/`else` except as a function
let fold
: ∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool
= λ(b : Bool) →
λ(bool : Type) →
λ(true : bool) →
λ(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

10
Bool/not.dhall
View file

@ -1,10 +0,0 @@
--| Flip the value of a `Bool`
let not
: Bool → Bool
= λ(b : Bool) → b == False
let example0 = assert : not True ≡ False
let example1 = assert : not False ≡ True
in not

20
Bool/odd.dhall
View file

@ -1,20 +0,0 @@
{-|
Returns `True` if there are an odd number of `True` elements in the list and
returns `False` otherwise.
This function is the `Monoid` for the `!=` operation.
-}
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

14
Bool/or.dhall
View file

@ -1,14 +0,0 @@
{-|
The `or` function returns `True` if there are any `True` elements in the `List`
and returns `False` otherwise
-}
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

13
Bool/package.dhall
View file

@ -1,12 +1 @@
λ(nix : ../NixPrelude.dhall) → λ(nix : ../NixPrelude.dhall) → { Type = Bool, fromAny = ./fromAny.dhall nix }
{ Type = Bool
, and = ./and.dhall
, build = ./build.dhall
, even = ./even.dhall
, fold = ./fold.dhall
, fromAny = ./fromAny.dhall nix
, not = ./not.dhall
, odd = ./odd.dhall
, or = ./or.dhall
, show = ./show.dhall
}

13
Bool/show.dhall
View file

@ -1,13 +0,0 @@
{-|
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"
let example0 = assert : show True ≡ "True"
let example1 = assert : show False ≡ "False"
in show

1
Double/package.dhall
View file

@ -23,7 +23,6 @@
, nonPositive = ./nonPositive.dhall nix , nonPositive = ./nonPositive.dhall nix
, positive = ./positive.dhall nix , positive = ./positive.dhall nix
, product = ./product.dhall nix , product = ./product.dhall nix
, show = ./show.dhall
, sort = ./sort.dhall nix , sort = ./sort.dhall nix
, subtract = ./subtract.dhall nix , subtract = ./subtract.dhall nix
, sum = ./sum.dhall nix , sum = ./sum.dhall nix

13
Double/show.dhall
View file

@ -1,13 +0,0 @@
{-|
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
let example0 = assert : show -3.1 ≡ "-3.1"
let example1 = assert : show 0.4 ≡ "0.4"
in show

17
Function/compose.dhall
View file

@ -1,17 +0,0 @@
--| Compose two functions into one.
let compose
: ∀(a : Type) → ∀(b : Type) → ∀(c : Type) → (a → b) → (b → c) → a → c
= λ(A : Type) →
λ(B : Type) →
λ(C : Type) →
λ(f : A → B) →
λ(g : B → C) →
λ(x : A) →
g (f x)
let example0 =
assert
: compose Natural Natural Bool (λ(n : Natural) → n + n) Natural/even 3
≡ True
in compose

10
Function/identity.dhall
View file

@ -1,10 +0,0 @@
--| The identity function simply returns its input
let identity
: ∀(a : Type) → ∀(x : a) → a
= λ(a : Type) → λ(x : a) → x
let example0 = assert : identity Natural 1 ≡ 1
let example1 = assert : identity Bool ≡ (λ(x : Bool) → x)
in identity

1
Function/package.dhall
View file

@ -1 +0,0 @@
{ compose = ./compose.dhall, identity = ./identity.dhall }

15
Integer/abs.dhall
View file

@ -1,15 +0,0 @@
--| Returns the absolute value of an `Integer`, i.e. its non-negative value.
let abs
: Integer → Natural
= λ(n : Integer) →
if Natural/isZero (Integer/clamp n)
then Integer/clamp (Integer/negate n)
else Integer/clamp n
let example0 = assert : abs +7 ≡ 7
let example2 = assert : abs +0 ≡ 0
let example3 = assert : abs -3 ≡ 3
in abs

22
Integer/add.dhall
View file

@ -1,22 +0,0 @@
--| `add m n` computes `m + n`.
let Integer/subtract = ./subtract.dhall
let add
: Integer → Integer → Integer
= λ(m : Integer) → λ(n : Integer) → Integer/subtract (Integer/negate m) n
let example0 = assert : add +3 +5 ≡ +8
let example1 = assert : add -3 -5 ≡ -8
let example2 = assert : add -4 +4 ≡ +0
let example3 = assert : add -3 +5 ≡ +2
let example4 = assert : add +3 -5 ≡ -2
let example5 = assert : add +0 -3 ≡ -3
let example6 = assert : add +0 +3 ≡ +3
in add

4
Integer/build.dhall
View file

@ -1,6 +1,6 @@
let Integer/add = ./add.dhall let Integer/add = https://prelude.dhall-lang.org/Integer/add.dhall
let negate = ./negate.dhall let negate = https://prelude.dhall-lang.org/Integer/negate.dhall
let Integer/succ let Integer/succ
: Integer → Integer : Integer → Integer

14
Integer/clamp.dhall
View file

@ -1,14 +0,0 @@
{-|
Convert an `Integer` to a `Natural` number, with negative numbers becoming zero.
-}
let clamp
: Integer → Natural
= Integer/clamp
let example0 = assert : clamp +7 ≡ 7
let example2 = assert : clamp +0 ≡ 0
let example3 = assert : clamp -3 ≡ 0
in clamp

21
Integer/equal.dhall
View file

@ -1,21 +0,0 @@
--| `equal` checks if two Integers are equal.
let Natural/equal = ../Natural/equal.dhall
let equal
: Integer → Integer → Bool
= λ(a : Integer) →
λ(b : Integer) →
Natural/equal (Integer/clamp a) (Integer/clamp b)
&& Natural/equal
(Integer/clamp (Integer/negate a))
(Integer/clamp (Integer/negate b))
let example0 = assert : equal +5 +5 ≡ True
let example1 = assert : equal +5 +6 ≡ False
let example2 = assert : equal +5 -5 ≡ False
let example3 = assert : equal -5 -5 ≡ True
in equal

4
Integer/fold.dhall
View file

@ -1,6 +1,6 @@
let Integer/negative = ./negative.dhall let Integer/negative = https://prelude.dhall-lang.org/Integer/negative.dhall
let Integer/abs = ./abs.dhall let Integer/abs = https://prelude.dhall-lang.org/Integer/abs.dhall
let fold let fold
: Integer → : Integer →

24
Integer/greaterThan.dhall
View file

@ -1,24 +0,0 @@
--| `greaterThan` checks if one Integer is greater than another.
let Bool/not = ../Bool/not.dhall
let lessThanEqual = ./lessThanEqual.dhall
let greaterThan
: Integer → Integer → Bool
= λ(x : Integer) → λ(y : Integer) → Bool/not (lessThanEqual x y)
let example0 = assert : greaterThan +5 +6 ≡ False
let example1 = assert : greaterThan +5 +5 ≡ False
let example2 = assert : greaterThan +5 +4 ≡ True
let example3 = assert : greaterThan -5 +8 ≡ False
let example4 = assert : greaterThan -5 -3 ≡ False
let example5 = assert : greaterThan -3 -5 ≡ True
let example6 = assert : greaterThan -3 -3 ≡ False
in greaterThan

24
Integer/greaterThanEqual.dhall
View file

@ -1,24 +0,0 @@
{-|
`greaterThanEqual` checks if one Integer is greater than or equal to another.
-}
let lessThanEqual = ./lessThanEqual.dhall
let greaterThanEqual
: Integer → Integer → Bool
= λ(x : Integer) → λ(y : Integer) → lessThanEqual y x
let example0 = assert : greaterThanEqual +5 +6 ≡ False
let example1 = assert : greaterThanEqual +5 +5 ≡ True
let example2 = assert : greaterThanEqual +5 +4 ≡ True
let example3 = assert : greaterThanEqual -5 +8 ≡ False
let example4 = assert : greaterThanEqual -5 -3 ≡ False
let example5 = assert : greaterThanEqual -3 -5 ≡ True
let example6 = assert : greaterThanEqual -3 -3 ≡ True
in greaterThanEqual

4
Integer/isZero.dhall
View file

@ -1,6 +1,6 @@
let Integer/nonPositive = ./nonPositive.dhall let Integer/nonPositive = https://prelude.dhall-lang.org/Integer/nonPositive.dhall
let Integer/nonNegative = ./nonNegative.dhall let Integer/nonNegative = https://prelude.dhall-lang.org/Integer/nonNegative.dhall
let isZero let isZero
: Integer → Bool : Integer → Bool

22
Integer/lessThan.dhall
View file

@ -1,22 +0,0 @@
--| `lessThan` checks if one Integer is less than another.
let greaterThan = ./greaterThan.dhall
let lessThan
: Integer → Integer → Bool
= λ(x : Integer) → λ(y : Integer) → greaterThan y x
let example0 = assert : lessThan +5 +6 ≡ True
let example1 = assert : lessThan +5 +5 ≡ False
let example2 = assert : lessThan +5 +4 ≡ False
let example3 = assert : lessThan -5 +8 ≡ True
let example4 = assert : lessThan -5 -3 ≡ True
let example5 = assert : lessThan -3 -5 ≡ False
let example6 = assert : lessThan -3 -3 ≡ False
in lessThan

35
Integer/lessThanEqual.dhall
View file

@ -1,35 +0,0 @@
--| `lessThanEqual` checks if one Integer is less than or equal to another.
let Natural/greaterThanEqual = ../Natural/greaterThanEqual.dhall
let Natural/lessThanEqual = ../Natural/lessThanEqual.dhall
let nonPositive = ./nonPositive.dhall
let nonNegative = ./nonNegative.dhall
let lessThanEqual
: Integer → Integer → Bool
= λ(x : Integer) →
λ(y : Integer) →
if nonPositive x
then nonNegative y
|| Natural/greaterThanEqual
(Integer/clamp (Integer/negate x))
(Integer/clamp (Integer/negate y))
else Natural/lessThanEqual (Integer/clamp x) (Integer/clamp y)
let example0 = assert : lessThanEqual +5 +6 ≡ True
let example1 = assert : lessThanEqual +5 +5 ≡ True
let example2 = assert : lessThanEqual +5 +4 ≡ False
let example3 = assert : lessThanEqual -5 +8 ≡ True
let example4 = assert : lessThanEqual -5 -3 ≡ True
let example5 = assert : lessThanEqual -3 -5 ≡ False
let example6 = assert : lessThanEqual -3 -3 ≡ True
in lessThanEqual

2
Integer/max.dhall
View file

@ -1,5 +1,5 @@
--| `max a b` returns the larger of `a` or `b` --| `max a b` returns the larger of `a` or `b`
let lessThanEqual = ./lessThanEqual.dhall let lessThanEqual = https://prelude.dhall-lang.org/Integer/lessThanEqual.dhall
let max let max
: Integer → Integer → Integer : Integer → Integer → Integer

2
Integer/min.dhall
View file

@ -1,5 +1,5 @@
--| `min a b` returns the smaller of `a` or `b` --| `min a b` returns the smaller of `a` or `b`
let lessThanEqual = ./lessThanEqual.dhall let lessThanEqual = https://prelude.dhall-lang.org/Integer/lessThanEqual.dhall
let min let min
: Integer → Integer → Integer : Integer → Integer → Integer

37
Integer/multiply.dhall
View file

@ -1,37 +0,0 @@
--| `multiply m n` computes `m * n`.
let nonPositive = ./nonPositive.dhall
let multiplyNonNegative =
λ(x : Integer) →
λ(y : Integer) →
Natural/toInteger (Integer/clamp x * Integer/clamp y)
let multiply
: Integer → Integer → Integer
= λ(m : Integer) →
λ(n : Integer) →
if nonPositive m
then if nonPositive n
then multiplyNonNegative (Integer/negate m) (Integer/negate n)
else Integer/negate (multiplyNonNegative (Integer/negate m) n)
else if nonPositive n
then Integer/negate (multiplyNonNegative m (Integer/negate n))
else multiplyNonNegative m n
let example0 = assert : multiply +3 +5 ≡ +15
let example1 = assert : multiply -3 +5 ≡ -15
let example2 = assert : multiply -3 -5 ≡ +15
let example3 = assert : multiply +0 +5 ≡ +0
let example4 = assert : multiply +5 +0 ≡ +0
let example5 = assert : multiply +0 +0 ≡ +0
let example6 = assert : multiply +1 +5 ≡ +5
let example7 = assert : multiply +3 -1 ≡ -3
in multiply

12
Integer/negate.dhall
View file

@ -1,12 +0,0 @@
--| Invert the sign of an `Integer`, with zero remaining unchanged.
let negate
: Integer → Integer
= Integer/negate
let example0 = assert : negate -3 ≡ +3
let example2 = assert : negate +7 ≡ -7
let example3 = assert : negate +0 ≡ +0
in negate

18
Integer/negative.dhall
View file

@ -1,18 +0,0 @@
{-|
Returns `True` for any `Integer` less than `+0`.
`negative` is more efficient than `./lessThan +0` or `./lessThanEqual -1`.
-}
let positive = ./positive.dhall
let negative
: Integer → Bool
= λ(n : Integer) → positive (Integer/negate n)
let example0 = assert : negative +1 ≡ False
let example1 = assert : negative +0 ≡ False
let example2 = assert : negative -1 ≡ True
in negative

18
Integer/nonNegative.dhall
View file

@ -1,18 +0,0 @@
{-|
Returns `True` for `+0` and any positive `Integer`.
`nonNegative` is more efficient than `./greaterThanEqual +0` or `./greaterThan -1`.
-}
let nonPositive = ./nonPositive.dhall
let nonNegative
: Integer → Bool
= λ(n : Integer) → nonPositive (Integer/negate n)
let example0 = assert : nonNegative +1 ≡ True
let example1 = assert : nonNegative +0 ≡ True
let example2 = assert : nonNegative -1 ≡ False
in nonNegative

16
Integer/nonPositive.dhall
View file

@ -1,16 +0,0 @@
{-|
Returns `True` for `+0` and any negative `Integer`.
`nonPositive` is more efficient than `./lessThanEqual +0` or `./lessThan +1`.
-}
let nonPositive
: Integer → Bool
= λ(n : Integer) → Natural/isZero (Integer/clamp n)
let example0 = assert : nonPositive +1 ≡ False
let example1 = assert : nonPositive +0 ≡ True
let example2 = assert : nonPositive -1 ≡ True
in nonPositive

21
Integer/package.dhall
View file

@ -1,33 +1,12 @@
λ(nix : ../NixPrelude.dhall) → λ(nix : ../NixPrelude.dhall) →
{ Type = Integer { Type = Integer
, abs = ./abs.dhall
, add = ./add.dhall
, build = ./build.dhall , build = ./build.dhall
, clamp = ./clamp.dhall
, divide = ./divide.dhall nix , divide = ./divide.dhall nix
, equal = ./equal.dhall
, fold = ./fold.dhall , fold = ./fold.dhall
, fromAny = ./fromAny.dhall nix , fromAny = ./fromAny.dhall nix
, greaterThan = ./greaterThan.dhall
, greaterThanEqual = ./greaterThanEqual.dhall
, isZero = ./isZero.dhall , isZero = ./isZero.dhall
, lessThan = ./lessThan.dhall
, lessThanEqual = ./lessThanEqual.dhall
, listMax = ./listMax.dhall nix , listMax = ./listMax.dhall nix
, listMin = ./listMin.dhall nix , listMin = ./listMin.dhall nix
, max = ./max.dhall
, min = ./min.dhall
, multiply = ./multiply.dhall
, negate = ./negate.dhall
, negative = ./negative.dhall
, nonNegative = ./nonNegative.dhall
, nonPositive = ./nonPositive.dhall
, positive = ./positive.dhall
, product = ./product.dhall , product = ./product.dhall
, show = ./show.dhall
, sort = ./sort.dhall nix , sort = ./sort.dhall nix
, subtract = ./subtract.dhall
, sum = ./sum.dhall
, toDouble = ./toDouble.dhall
, toNatural = ./toNatural.dhall
} }

20
Integer/positive.dhall
View file

@ -1,20 +0,0 @@
{-|
Returns `True` for any `Integer` greater than `+0`.
`positive` is more efficient than `./greaterThan +0` or `./greaterThanEqual +1`.
-}
let not = ../Bool/not.dhall
let nonPositive = ./nonPositive.dhall
let positive
: Integer → Bool
= λ(n : Integer) → not (nonPositive n)
let example0 = assert : positive +1 ≡ True
let example1 = assert : positive +0 ≡ False
let example2 = assert : positive -1 ≡ False
in positive

2
Integer/product.dhall
View file

@ -1,5 +1,5 @@
--| Multiply all the numbers in a `List` --| Multiply all the numbers in a `List`
let Integer/multiply = ./multiply.dhall let Integer/multiply = https://prelude.dhall-lang.org/Integer/multiply.dhall
let product let product
: List Integer → Integer : List Integer → Integer

14
Integer/show.dhall
View file

@ -1,14 +0,0 @@
{-|
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
let example0 = assert : show -3 ≡ "-3"
let example1 = assert : show +0 ≡ "+0"
in show

51
Integer/subtract.dhall
View file

@ -1,51 +0,0 @@
--| `subtract m n` computes `n - m`.
let nonPositive = ./nonPositive.dhall
let subtractNonNegative =
λ(xi : Integer) →
λ(yi : Integer) →
let xn = Integer/clamp xi
let yn = Integer/clamp yi
let dn = Natural/subtract xn yn
in if Natural/isZero dn
then Integer/negate (Natural/toInteger (Natural/subtract yn xn))
else Natural/toInteger dn
let subtract
: Integer → Integer → Integer
= λ(m : Integer) →
λ(n : Integer) →
if nonPositive m
then if nonPositive n
then subtractNonNegative (Integer/negate n) (Integer/negate m)
else Natural/toInteger
(Integer/clamp (Integer/negate m) + Integer/clamp n)
else if nonPositive n
then Integer/negate
( Natural/toInteger
(Integer/clamp m + Integer/clamp (Integer/negate n))
)
else subtractNonNegative m n
let example0 = assert : subtract +3 +5 ≡ +2
let example1 = assert : subtract +4 +4 ≡ +0
let example2 = assert : subtract +5 +3 ≡ -2
let example3 = assert : subtract -3 -5 ≡ -2
let example4 = assert : subtract -4 -4 ≡ +0
let example5 = assert : subtract -5 -3 ≡ +2
let example6 = assert : subtract -3 +5 ≡ +8
let example7 = assert : subtract +3 -5 ≡ -8
let example8 = assert : subtract +0 -3 ≡ -3
in subtract

10
Integer/toDouble.dhall
View file

@ -1,10 +0,0 @@
--| Convert an `Integer` to the corresponding `Double`
let toDouble
: Integer → Double
= Integer/toDouble
let example0 = assert : toDouble -3 ≡ -3.0
let example1 = assert : toDouble +2 ≡ 2.0
in toDouble

17
Integer/toNatural.dhall
View file

@ -1,17 +0,0 @@
{-|
Convert an `Integer` to an `Optional Natural`, with negative numbers becoming `None Natural`.
-}
let nonNegative = ./nonNegative.dhall
let toNatural
: Integer → Optional Natural
= λ(n : Integer) →
if nonNegative n then Some (Integer/clamp n) else None Natural
let example0 = assert : toNatural +7 ≡ Some 7
let example2 = assert : toNatural +0 ≡ Some 0
let example3 = assert : toNatural -3 ≡ None Natural
in toNatural

7
JSON/Format.dhall
View file

@ -1,7 +0,0 @@
{-|
An internal type used by `./renderAs` to select the output format.
You should not need to use this type directly, simply use `./render`
or `./renderYAML` as appropriate.
-}
< YAML | JSON >

35
JSON/Nesting.dhall
View file

@ -1,35 +0,0 @@
{-|
This type is used as part of `dhall-json`'s support for preserving alternative
names
For example, this Dhall code:
```
let Example = < Left : { foo : Natural } | Right : { bar : Bool } >
let Nesting = < Inline | Nested : Text >
in { field =
"name"
, nesting =
Nesting.Inline
, contents =
Example.Left { foo = 2 }
}
```
... generates this JSON:
```
{
"foo": 2,
"name": "Left"
}
```
-}
let Nesting
: Type
= < Inline | Nested : Text >
in Nesting

67
JSON/Tagged.dhall
View file

@ -1,67 +0,0 @@
{-|
This is a convenient type-level function when using `dhall-to-json`'s support
for preserving alternative names
For example, this code:
```
let map = ../List/map
let Provisioner =
< shell :
{ inline : List Text }
| file :
{ source : Text, destination : Text }
>
let Tagged = ./Tagged
let Nesting = ./Nesting
let wrap
: Provisioner → Tagged Provisioner
= λ(x : Provisioner) →
{ field = "type", nesting = Nesting.Nested "params", contents = x }
in { provisioners =
map
Provisioner
(Tagged Provisioner)
wrap
[ Provisioner.shell { inline = [ "echo foo" ] }
, Provisioner.file
{ source = "app.tar.gz", destination = "/tmp/app.tar.gz" }
]
}
```
... produces this JSON:
```
{
"provisioners": [
{
"params": {
"inline": [
"echo foo"
]
},
"type": "shell"
},
{
"params": {
"destination": "/tmp/app.tar.gz",
"source": "app.tar.gz"
},
"type": "file"
}
]
}
```
-}
let Tagged
: Type → Type
= λ(a : Type) → { field : Text, nesting : ./Nesting.dhall, contents : a }
in Tagged

63
JSON/Type.dhall
View file

@ -1,63 +0,0 @@
{-|
Dhall encoding of an arbitrary JSON value
For example, the following JSON value:
```
[ { "foo": null, "bar": [ 1.0, true ] } ]
```
... corresponds to the following Dhall expression:
```
λ(JSON : Type) →
λ ( json
: { array : List JSON → JSON
, bool : Bool → JSON
, null : JSON
, double : Double → JSON
, integer : Integer → JSON
, object : List { mapKey : Text, mapValue : JSON } → JSON
, string : Text → JSON
}
) →
json.object
[ { mapKey = "foo", mapValue = json.null }
, { mapKey = "bar"
, mapValue = json.array [ json.double 1.0, json.bool True ]
}
]
```
You do not need to create these values directly, though. You can use
the utilities exported by `./package.dhall` to create values of this type,
such as:
```
let JSON = ./package.dhall
in JSON.object
[ { mapKey = "foo", mapValue = JSON.null }
, { mapKey = "bar"
, mapValue = JSON.array [ JSON.double 1.0, JSON.bool True ]
}
]
```
-}
let JSON/Type
: Type
= ∀(JSON : Type) →
∀ ( json
: { array : List JSON → JSON
, bool : Bool → JSON
, double : Double → JSON
, integer : Integer → JSON
, null : JSON
, object : List { mapKey : Text, mapValue : JSON } → JSON
, string : Text → JSON
}
) →
JSON
in JSON/Type

35
JSON/array.dhall
View file

@ -1,35 +0,0 @@
{-|
Create a JSON array from a `List` of JSON values
```
let JSON = ./package.dhall
in JSON.render (JSON.array [ JSON.double 1.0, JSON.bool True ])
= "[ 1.0, true ]"
let JSON/Type = ./Type
let JSON = ./package.dhall
in JSON.render (JSON.array ([] : List JSON/Type))
= "[ ]"
```
-}
let JSON = ./Type.dhall
let List/map = ../List/map.dhall
let array
: List JSON → JSON
= λ(x : List JSON) →
λ(JSON : Type) →
λ ( json
: { array : List JSON → JSON
, bool : Bool → JSON
, double : Double → JSON
, integer : Integer → JSON
, null : JSON
, object : List { mapKey : Text, mapValue : JSON } → JSON
, string : Text → JSON
}
) →
json.array (List/map JSON@1 JSON (λ(j : JSON@1) → j JSON json) x)
in array

32
JSON/bool.dhall
View file

@ -1,32 +0,0 @@
{-|
Create a JSON bool from a Dhall `Bool`
```
let JSON = ./package.dhall
in JSON.render (JSON.bool True)
= "true"
let JSON = ./package.dhall
in JSON.render (JSON.bool False)
= "false"
```
-}
let JSON = ./Type.dhall
let bool
: Bool → JSON
= λ(x : Bool) →
λ(JSON : Type) →
λ ( json
: { array : List JSON → JSON
, bool : Bool → JSON
, double : Double → JSON
, integer : Integer → JSON
, null : JSON
, object : List { mapKey : Text, mapValue : JSON } → JSON
, string : Text → JSON
}
) →
json.bool x
in bool

25
JSON/core.dhall
View file

@ -1,25 +0,0 @@
{-|
A record of functions useful for constructing `JSON` values.
This is only a subset of what `package.dhall` exports. If you are not writing a
JSON prelude function, you should use the `package.dhall` file instead.
It is used internally by `render`, `renderYAML` and `omitNullFields` instead of
`package.dhall` to avoid import cycles.
-}
{ Type = ./Type.dhall
, Tagged = ./Tagged.dhall
, Nesting = ./Nesting.dhall
, keyText = ./keyText.dhall
, keyValue = ./keyValue.dhall
, string = ./string.dhall
, number = ./number.dhall
, double = ./double.dhall
, integer = ./integer.dhall
, natural = ./natural.dhall
, object = ./object.dhall
, array = ./array.dhall
, bool = ./bool.dhall
, null = ./null.dhall
, renderInteger = ./renderInteger.dhall
}

32
JSON/double.dhall
View file

@ -1,32 +0,0 @@
{-|
Create a JSON number from a Dhall `Double`
```
let JSON = ./package.dhall
in JSON.render (JSON.double 42.0)
= "42.0"
let JSON = ./package.dhall
in JSON.render (JSON.double -1.5e-10)
= "-1.5e-10"
```
-}
let JSON = ./Type.dhall
let double
: Double → JSON
= λ(x : Double) →
λ(JSON : Type) →
λ ( json
: { array : List JSON → JSON
, bool : Bool → JSON
, double : Double → JSON
, integer : Integer → JSON
, null : JSON
, object : List { mapKey : Text, mapValue : JSON } → JSON
, string : Text → JSON
}
) →
json.double x
in double

32
JSON/integer.dhall
View file

@ -1,32 +0,0 @@
{-|
Create a JSON number from a Dhall `Integer`
```
let JSON = ./package.dhall
in JSON.render (JSON.integer -1)
= "-1"
let JSON = ./package.dhall
in JSON.render (JSON.integer +2)
= "+2"
```
-}
let JSON = ./Type.dhall
let integer
: Integer → JSON
= λ(x : Integer) →
λ(JSON : Type) →
λ ( json
: { array : List JSON → JSON
, bool : Bool → JSON
, double : Double → JSON
, integer : Integer → JSON
, null : JSON
, object : List { mapKey : Text, mapValue : JSON } → JSON
, string : Text → JSON
}
) →
json.integer x
in integer

1
JSON/keyText.dhall
View file

@ -1 +0,0 @@
../Map/keyText.dhall

1
JSON/keyValue.dhall
View file

@ -1 +0,0 @@
../Map/keyValue.dhall

28
JSON/natural.dhall
View file

@ -1,28 +0,0 @@
{-|
Create a JSON number from a Dhall `Natural`
```
let JSON = ./package.dhall
in JSON.render (JSON.natural 42)
= "42"
```
-}
let JSON = ./Type.dhall
let natural
: Natural → JSON
= λ(x : Natural) →
λ(JSON : Type) →
λ ( json
: { array : List JSON → JSON
, bool : Bool → JSON
, double : Double → JSON
, integer : Integer → JSON
, null : JSON
, object : List { mapKey : Text, mapValue : JSON } → JSON
, string : Text → JSON
}
) →
json.integer (Natural/toInteger x)
in natural

27
JSON/null.dhall
View file

@ -1,27 +0,0 @@
{-|
Create a JSON null
```
let JSON = ./package.dhall
in JSON.render JSON.null
= "null"
```
-}
let JSON = ./Type.dhall
let null
: JSON
= λ(JSON : Type) →
λ ( json
: { array : List JSON → JSON
, bool : Bool → JSON
, double : Double → JSON
, integer : Integer → JSON
, null : JSON
, object : List { mapKey : Text, mapValue : JSON } → JSON
, string : Text → JSON
}
) →
json.null
in null

22
JSON/number.dhall
View file

@ -1,22 +0,0 @@
{-|
Create a JSON number from a Dhall `Double`
```
let JSON = ./package.dhall
in JSON.render (JSON.number 42.0)
= "42.0"
let JSON = ./package.dhall
in JSON.render (JSON.number -1.5e-10)
= "-1.5e-10"
```
-}
let JSON = ./Type.dhall
let double = ./double.dhall
let number
: Double → JSON
= double
in number

49
JSON/object.dhall
View file

@ -1,49 +0,0 @@
{-|
Create a JSON object from a Dhall `Map`
```
let JSON = ./package.dhall
in JSON.render
( JSON.object
[ { mapKey = "foo", mapValue = JSON.double 1.0 }
, { mapKey = "bar", mapValue = JSON.bool True }
]
)
= "{ \"foo\": 1.0, \"bar\": true }"
let JSON/Type = ./Type
let JSON = ./package.dhall
in JSON.render
(JSON.object ([] : List { mapKey : Text, mapValue : JSON/Type }))
= "{ }"
```
-}
let JSON = ./Type.dhall
let List/map = ../List/map.dhall
let object
: List { mapKey : Text, mapValue : JSON } → JSON
= λ(x : List { mapKey : Text, mapValue : JSON }) →
λ(JSON : Type) →
λ ( json
: { array : List JSON → JSON
, bool : Bool → JSON
, double : Double → JSON
, integer : Integer → JSON
, null : JSON
, object : List { mapKey : Text, mapValue : JSON } → JSON
, string : Text → JSON
}
) →
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 }
)
x
)
in object

136
JSON/omitNullFields.dhall
View file

@ -1,136 +0,0 @@
{-|
This utility omits all `null` record fields, which is often the idiomatic way
for a configuration to encode absent fields
-}
let JSON = ./core.dhall
let List/concatMap = ../List/concatMap.dhall
let List/map = ../List/map.dhall
let omitNullFields
: JSON.Type → JSON.Type
= λ(old : JSON.Type) →
λ(JSON : Type) →
λ ( json
: { array : List JSON → JSON
, bool : Bool → JSON
, double : Double → JSON
, integer : Integer → JSON
, null : JSON
, object : List { mapKey : Text, mapValue : JSON } → JSON
, string : Text → JSON
}
) →
let result =
old
{ value : JSON, isNull : Bool }
{ string =
λ(x : Text) → { value = json.string x, isNull = False }
, double =
λ(x : Double) → { value = json.double x, isNull = False }
, integer =
λ(x : Integer) → { value = json.integer x, isNull = False }
, object =
λ ( keyValues
: List
{ mapKey : Text
, mapValue : { value : JSON, isNull : Bool }
}
) →
let value =
json.object
( List/concatMap
{ mapKey : Text
, mapValue : { value : JSON, isNull : Bool }
}
{ mapKey : Text, mapValue : JSON }
( λ ( keyValue
: { mapKey : Text
, mapValue :
{ value : JSON, isNull : Bool }
}
) →
if keyValue.mapValue.isNull
then [] : List
{ mapKey : Text
, mapValue : JSON
}
else [ keyValue.{ mapKey }
∧ { mapValue =
keyValue.mapValue.value
}
]
)
keyValues
)
in { value, isNull = False }
, array =
λ(xs : List { value : JSON, isNull : Bool }) →
let value =
json.array
( List/map
{ value : JSON, isNull : Bool }
JSON
( λ(x : { value : JSON, isNull : Bool }) →
x.value
)
xs
)
in { value, isNull = False }
, bool = λ(x : Bool) → { value = json.bool x, isNull = False }
, null = { value = json.null, isNull = True }
}
in result.value
let property =
λ(a : Text) →
λ(b : Double) →
λ(c : Bool) →
assert
: omitNullFields
( JSON.object
( toMap
{ string = JSON.string a
, double = JSON.double b
, bool = JSON.bool c
, null = JSON.null
}
)
)
≡ JSON.object
( toMap
{ string = JSON.string a
, double = JSON.double b
, bool = JSON.bool c
}
)
let example =
assert
: omitNullFields
( JSON.object
( toMap
{ array =
JSON.array [ JSON.object (toMap { null = JSON.null }) ]
}
)
)
≡ JSON.object
( toMap
{ array =
JSON.array
[ JSON.object
([] : List { mapKey : Text, mapValue : JSON.Type })
]
}
)
let example =
assert
: omitNullFields (JSON.array [ JSON.null ]) ≡ JSON.array [ JSON.null ]
in omitNullFields

9
JSON/package.dhall
View file

@ -1,9 +0,0 @@
λ(nix : ../NixPrelude.dhall) →
{ render = ./render.dhall nix
, renderCompact = ./renderCompact.dhall
, renderYAML = ./renderYAML.dhall nix
, omitNullFields = ./omitNullFields.dhall
, tagInline = ./tagInline.dhall
, tagNested = ./tagNested.dhall
}
∧ ./core.dhall

12
JSON/render.dhall
View file

@ -1,12 +0,0 @@
λ(nix : ../NixPrelude.dhall) →
let JSON = ./core.dhall
let Format = ./Format.dhall
let renderAs = ./renderAs.dhall nix
let render
: JSON.Type → Text
= renderAs Format.JSON
in render

296
JSON/renderAs.dhall
View file

@ -1,296 +0,0 @@
--| Render a `JSON` value as `Text` in either JSON or YAML format.
λ(nix : ../NixPrelude.dhall) →
let JSON = ./core.dhall
let Function/identity = ../Function/identity.dhall
let Text/concatMap = ../Text/concatMap.dhall
let List/map = ../List/map.dhall
let NonEmpty = ../NonEmpty/Type.dhall
let NonEmpty/toList = ../NonEmpty/toList.dhall
let NonEmpty/concat = ../NonEmpty/concat.dhall
let NonEmpty/map = ../NonEmpty/map.dhall
let NonEmpty/singleton = ../NonEmpty/singleton.dhall
let Optional/fold = ../Optional/fold.dhall nix
let List/uncons
: ∀(a : Type) → List a → Optional (NonEmpty a)
= {- This version uses the `ls` argument only once to prevent cache blowups at the price
of performing two passes over the list:
A first one to reverse it, a second one with `List/fold` to determine
the head element.
See https://github.com/dhall-lang/dhall-lang/pull/1015#issuecomment-633381024
for some context regarding the caching issue.
-}
λ(a : Type) →
λ(ls : List a) →
List/fold
a
(List/reverse a ls)
(Optional (NonEmpty a))
( λ(x : a) →
λ(acc : Optional (NonEmpty a)) →
Optional/fold
(NonEmpty a)
acc
(Optional (NonEmpty a))
(λ(ne : NonEmpty a) → Some (ne ⫽ { tail = ne.tail # [ x ] }))
(Some (NonEmpty/singleton a x))
)
(None (NonEmpty a))
let NonEmpty/mapHead
: ∀(a : Type) → (a → a) → NonEmpty a → NonEmpty a
= λ(a : Type) →
λ(fn : a → a) →
λ(ls : NonEmpty a) →
ls ⫽ { head = fn ls.head }
let NonEmpty/mapTail
: ∀(a : Type) → (a → a) → NonEmpty a → NonEmpty a
= λ(a : Type) →
λ(fn : a → a) →
λ(ls : NonEmpty a) →
ls ⫽ { tail = List/map a a fn ls.tail }
let NonEmpty/prepend
: ∀(a : Type) → a → NonEmpty a → NonEmpty a
= λ(a : Type) →
λ(prefix : a) →
λ(ls : NonEmpty a) →
{ head = prefix, tail = NonEmpty/toList a ls }
let NonYtpme
: Type → Type
= λ(a : Type) → { init : List a, last : a }
let List/unsnoc
: ∀(a : Type) → List a → Optional (NonYtpme a)
= λ(a : Type) →
λ(ls : List a) →
List/fold
a
ls
(Optional (NonYtpme a))
( λ(x : a) →
λ(acc : Optional (NonYtpme a)) →
Optional/fold
(NonYtpme a)
acc
(Optional (NonYtpme a))
(λ(ny : NonYtpme a) → Some (ny ⫽ { init = [ x ] # ny.init }))
(Some { init = [] : List a, last = x })
)
(None (NonYtpme a))
let NonEmpty/mapLast
: ∀(a : Type) → (a → a) → NonEmpty a → NonEmpty a
= λ(a : Type) →
λ(fn : a → a) →
λ(ls : NonEmpty a) →
Optional/fold
(NonYtpme a)
(List/unsnoc a ls.tail)
(NonEmpty a)
(λ(x : NonYtpme a) → ls ⫽ { tail = x.init # [ fn x.last ] })
(NonEmpty/singleton a (fn ls.head))
let NonEmpty/mapLeading
: ∀(a : Type) → (a → a) → NonEmpty a → NonEmpty a
= λ(a : Type) →
λ(fn : a → a) →
λ(ls : NonEmpty a) →
Optional/fold
(NonYtpme a)
(List/unsnoc a ls.tail)
(NonEmpty a)
( λ(x : NonYtpme a) →
{ head = fn ls.head
, tail = List/map a a fn x.init # [ x.last ]
}
)
ls
let Lines
: Type
= NonEmpty Text
let Block
: Type
= < Simple : Text | Complex : Lines >
let Block/toLines
: Block → Lines
= λ(block : Block) →
merge
{ Simple = NonEmpty/singleton Text
, Complex = Function/identity Lines
}
block
let manyBlocks
: ∀(a : Type) → Text → (NonEmpty a → Lines) → List a → Block
= λ(a : Type) →
λ(ifEmpty : Text) →
λ(render : NonEmpty a → Lines) →
λ(inputs : List a) →
Optional/fold
(NonEmpty a)
(List/uncons a inputs)
Block
(λ(inputs : NonEmpty a) → Block.Complex (render inputs))
(Block.Simple ifEmpty)
let blockToText
: Block → Text
= λ(block : Block) →
Text/concatMap
Text
(λ(line : Text) → line ++ "\n")
(NonEmpty/toList Text (Block/toLines block))
let addPrefix = λ(prefix : Text) → λ(line : Text) → prefix ++ line
let addIndent = addPrefix " "
let indentTail = NonEmpty/mapTail Text addIndent
let Format =
./Format.dhall
let ObjectField = { mapKey : Text, mapValue : Block }
let -- Essentially the same thing as `Text/show`, except that this does not
-- escape `$`
escape =
List/fold
(Text → Text)
[ Text/replace "\"" "\\\""
, Text/replace "\b" "\\b"
, Text/replace "\f" "\\f"
, Text/replace "\n" "\\n"
, Text/replace "\r" "\\r"
, Text/replace "\t" "\\t"
, Text/replace "\\" "\\\\"
]
Text
(λ(replace : Text → Text) → λ(text : Text) → replace text)
let renderJSONStruct =
λ(prefix : Text) →
λ(suffix : Text) →
λ(blocks : NonEmpty Lines) →
let indent = List/map Text Text addIndent
let appendComma
: Lines → Lines
= NonEmpty/mapLast Text (λ(line : Text) → line ++ ",")
let blocks = NonEmpty/mapLeading Lines appendComma blocks
let block = NonEmpty/concat Text blocks
in Optional/fold
(NonYtpme Text)
(List/unsnoc Text block.tail)
(NonEmpty Text)
( λ(ny : NonYtpme Text) →
{ head = prefix
, tail =
indent ([ block.head ] # ny.init # [ ny.last ])
# [ suffix ]
}
)
(NonEmpty/singleton Text "${prefix} ${block.head} ${suffix}")
let renderObject =
λ(format : Format) →
λ(fields : NonEmpty ObjectField) →
let keystr = λ(field : ObjectField) → "\"${escape field.mapKey}\":"
let prefixKeyOnFirst =
λ(field : ObjectField) →
NonEmpty/mapHead
Text
(addPrefix "${keystr field} ")
(Block/toLines field.mapValue)
let prependKeyLine =
λ(field : ObjectField) →
NonEmpty/prepend
Text
(keystr field)
(Block/toLines field.mapValue)
let renderYAMLField =
λ(field : ObjectField) →
merge
{ Simple =
λ(line : Text) →
NonEmpty/singleton Text "${keystr field} ${line}"
, Complex = λ(_ : Lines) → indentTail (prependKeyLine field)
}
field.mapValue
in merge
{ JSON =
renderJSONStruct
"{"
"}"
(NonEmpty/map ObjectField Lines prefixKeyOnFirst fields)
, YAML =
NonEmpty/concat
Text
(NonEmpty/map ObjectField Lines renderYAMLField fields)
}
format
let renderYAMLArrayField =
λ(block : Block) →
NonEmpty/mapHead
Text
(addPrefix "- ")
(indentTail (Block/toLines block))
let renderArray =
λ(format : Format) →
λ(fields : NonEmpty Block) →
merge
{ JSON =
renderJSONStruct
"["
"]"
(NonEmpty/map Block Lines Block/toLines fields)
, YAML =
NonEmpty/concat
Text
(NonEmpty/map Block Lines renderYAMLArrayField fields)
}
format
let renderAs
: Format → JSON.Type → Text
= λ(format : Format) →
λ(json : JSON.Type) →
blockToText
( json
Block
{ string = λ(x : Text) → Block.Simple "\"${escape x}\""
, double = λ(x : Double) → Block.Simple (Double/show x)
, integer = λ(x : Integer) → Block.Simple (JSON.renderInteger x)
, object = manyBlocks ObjectField "{}" (renderObject format)
, array = manyBlocks Block "[]" (renderArray format)
, bool =
λ(x : Bool) → Block.Simple (if x then "true" else "false")
, null = Block.Simple "null"
}
)
in renderAs

52
JSON/renderCompact.dhall
View file

@ -1,52 +0,0 @@
--| This renders JSON on a single line
let JSON = ./core.dhall
let Text/concatMapSep = ../Text/concatMapSep.dhall
let renderInteger = ./renderInteger.dhall
let renderCompact
: JSON.Type → Text
= λ(j : JSON.Type) →
j
Text
{ string = Text/show
, double = Double/show
, integer = renderInteger
, object =
λ(x : List { mapKey : Text, mapValue : Text }) →
let body =
Text/concatMapSep
","
{ mapKey : Text, mapValue : Text }
( λ(e : { mapKey : Text, mapValue : Text }) →
" ${Text/show e.mapKey}: ${e.mapValue}"
)
x
in "{${body} }"
, array =
λ(x : List Text) →
let body = Text/concatMapSep "," Text (λ(y : Text) → " ${y}") x
in "[${body} ]"
, bool = λ(x : Bool) → if x then "true" else "false"
, null = "null"
}
let example =
assert
: renderCompact
( JSON.array
[ JSON.bool True
, JSON.string "Hello"
, JSON.object
[ { mapKey = "foo", mapValue = JSON.null }
, { mapKey = "bar", mapValue = JSON.double 1.1 }
, { mapKey = "baz", mapValue = JSON.integer +2 }
]
]
)
≡ "[ true, \"Hello\", { \"foo\": null, \"bar\": 1.1, \"baz\": 2 } ]"
in renderCompact

20
JSON/renderInteger.dhall
View file

@ -1,20 +0,0 @@
{-|
Render an `Integer` value as a `JSON number`, according to the JSON standard, in
which a number may not start with a plus sign (`+`).
-}
let Integer/nonNegative = ../Integer/nonNegative.dhall
let renderInteger
: Integer → Text
= λ(integer : Integer) →
if Integer/nonNegative integer
then Natural/show (Integer/clamp integer)
else Integer/show integer
let positive = assert : renderInteger +1 ≡ "1"
let zero = assert : renderInteger +0 ≡ "0"
let negative = assert : renderInteger -1 ≡ "-1"
in renderInteger

12
JSON/renderYAML.dhall
View file

@ -1,12 +0,0 @@
λ(nix : ../NixPrelude.dhall) →
let JSON = ./core.dhall
let Format = ./Format.dhall
let renderAs = ./renderAs.dhall nix
let renderYAML
: JSON.Type → Text
= renderAs Format.YAML
in renderYAML

32
JSON/string.dhall
View file

@ -1,32 +0,0 @@
{-|
Create a JSON string from Dhall `Text`
```
let JSON = ./package.dhall
in JSON.render (JSON.string "ABC $ \" 🙂")
= "\"ABC \\u0024 \\\" 🙂\""
let JSON = ./package.dhall
in JSON.render (JSON.string "")
= "\"\""
```
-}
let JSON = ./Type.dhall
let string
: Text → JSON
= λ(x : Text) →
λ(JSON : Type) →
λ ( json
: { array : List JSON → JSON
, bool : Bool → JSON
, double : Double → JSON
, integer : Integer → JSON
, null : JSON
, object : List { mapKey : Text, mapValue : JSON } → JSON
, string : Text → JSON
}
) →
json.string x
in string

23
JSON/tagInline.dhall
View file

@ -1,23 +0,0 @@
--| Prepare a union value for JSON- or YAML-encoding with the inline layout
let Nesting = ./Nesting.dhall
let Tagged = ./Tagged.dhall
let tagInline
: Text → ∀(a : Type) → a → Tagged a
= λ(tagFieldName : Text) →
λ(a : Type) →
λ(contents : a) →
{ nesting = Nesting.Inline, field = tagFieldName, contents }
let example0 =
let Example = < Left : { foo : Natural } | Right : { bar : Bool } >
in assert
: tagInline "name" Example (Example.Left { foo = 2 })
≡ { field = "name"
, nesting = Nesting.Inline
, contents = Example.Left { foo = 2 }
}
in tagInline

27
JSON/tagNested.dhall
View file

@ -1,27 +0,0 @@
--| Prepare a union value for JSON- or YAML-encoding with the nested layout
let Nesting = ./Nesting.dhall
let Tagged = ./Tagged.dhall
let tagNested
: Text → Text → ∀(a : Type) → a → Tagged a
= λ(contentsFieldName : Text) →
λ(tagFieldName : Text) →
λ(a : Type) →
λ(contents : a) →
{ nesting = Nesting.Nested contentsFieldName
, field = tagFieldName
, contents
}
let example0 =
let Example = < Left : { foo : Natural } | Right : { bar : Bool } >
in assert
: tagNested "value" "name" Example (Example.Left { foo = 2 })
≡ { field = "name"
, nesting = Nesting.Nested "value"
, contents = Example.Left { foo = 2 }
}
in tagNested

16
List/all.dhall
View file

@ -1,16 +0,0 @@
{-|
Returns `True` if the supplied function returns `True` for all elements in the
`List`
-}
let all
: ∀(a : Type) → (a → Bool) → List a → Bool
= λ(a : Type) →
λ(f : a → Bool) →
λ(xs : List a) →
List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x && r) True
let example0 = assert : all Natural Natural/even [ 2, 3, 5 ] ≡ False
let example1 = assert : all Natural Natural/even ([] : List Natural) ≡ True
in all

16
List/any.dhall
View file

@ -1,16 +0,0 @@
{-|
Returns `True` if the supplied function returns `True` for any element in the
`List`
-}
let any
: ∀(a : Type) → (a → Bool) → List a → Bool
= λ(a : Type) →
λ(f : a → Bool) →
λ(xs : List a) →
List/fold a xs Bool (λ(x : a) → λ(r : Bool) → f x || r) False
let example0 = assert : any Natural Natural/even [ 2, 3, 5 ] ≡ True
let example1 = assert : any Natural Natural/even ([] : List Natural) ≡ False
in any

30
List/build.dhall
View file

@ -1,30 +0,0 @@
--| `build` is the inverse of `fold`
let build
: ∀(a : Type) →
(∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list) →
List a
= List/build
let example0 =
assert
: build
Text
( λ(list : Type) →
λ(cons : Text → list → list) →
λ(nil : list) →
cons "ABC" (cons "DEF" nil)
)
≡ [ "ABC", "DEF" ]
let example1 =
assert
: build
Text
( λ(list : Type) →
λ(cons : Text → list → list) →
λ(nil : list) →
nil
)
≡ ([] : List Text)
in build

34
List/concat.dhall
View file

@ -1,34 +0,0 @@
--| Concatenate a `List` of `List`s into a single `List`
let concat
: ∀(a : Type) → List (List a) → List a
= λ(a : Type) →
λ(xss : List (List a)) →
List/build
a
( λ(list : Type) →
λ(cons : a → list → list) →
λ(nil : list) →
List/fold
(List a)
xss
list
(λ(xs : List a) → λ(ys : list) → List/fold a xs list cons ys)
nil
)
let example0 =
assert
: concat Natural [ [ 0, 1, 2 ], [ 3, 4 ], [ 5, 6, 7, 8 ] ]
≡ [ 0, 1, 2, 3, 4, 5, 6, 7, 8 ]
let example1 =
assert
: concat
Natural
[ [] : List Natural, [] : List Natural, [] : List Natural ]
≡ ([] : List Natural)
let example2 =
assert : concat Natural ([] : List (List Natural)) ≡ ([] : List Natural)
in concat

32
List/concatMap.dhall
View file

@ -1,32 +0,0 @@
{-|
Transform a list by applying a function to each element and flattening the
results
-}
let concatMap
: ∀(a : Type) → ∀(b : Type) → (a → List b) → List a → List b
= λ(a : Type) →
λ(b : Type) →
λ(f : a → List b) →
λ(xs : List a) →
List/build
b
( λ(list : Type) →
λ(cons : b → list → list) →
List/fold a xs list (λ(x : a) → List/fold b (f x) list cons)
)
let example0 =
assert
: concatMap Natural Natural (λ(n : Natural) → [ n, n ]) [ 2, 3, 5 ]
≡ [ 2, 2, 3, 3, 5, 5 ]
let example1 =
assert
: concatMap
Natural
Natural
(λ(n : Natural) → [ n, n ])
([] : List Natural)
≡ ([] : List Natural)
in concatMap

10
List/default.dhall
View file

@ -1,10 +0,0 @@
λ(nix : ../NixPrelude.dhall) →
let Optional/default = ../Optional/default.dhall nix
let default
: ∀(a : Type) → Optional (List a) → List a
= λ(a : Type) →
λ(o : Optional (List a)) →
Optional/default (List a) ([] : List a) o
in default

25
List/drop.dhall
View file

@ -1,25 +0,0 @@
--| Remove first `n` elements of a list
let Natural/greaterThanEqual = ../Natural/greaterThanEqual.dhall
let drop
: ∀(n : Natural) → ∀(a : Type) → List a → List a
= λ(n : Natural) →
λ(a : Type) →
λ(xs : List a) →
List/fold
{ index : Natural, value : a }
(List/indexed a xs)
(List a)
( λ(x : { index : Natural, value : a }) →
λ(xs : List a) →
if Natural/greaterThanEqual x.index n
then [ x.value ] # xs
else xs
)
([] : List a)
let example = assert : drop 2 Natural [ 2, 3, 5 ] ≡ [ 5 ]
let example = assert : drop 5 Natural [ 2, 3, 5 ] ≡ ([] : List Natural)
in drop

8
List/empty.dhall
View file

@ -1,8 +0,0 @@
--| An empty list of the given type
let empty
: ∀(a : Type) → List a
= λ(a : Type) → [] : List a
let example0 = assert : empty Bool ≡ ([] : List Bool)
in empty

22
List/filter.dhall
View file

@ -1,22 +0,0 @@
--| Only keep elements of the list where the supplied function returns `True`
let filter
: ∀(a : Type) → (a → Bool) → List a → List a
= λ(a : Type) →
λ(f : a → Bool) →
λ(xs : List a) →
List/build
a
( λ(list : Type) →
λ(cons : a → list → list) →
List/fold
a
xs
list
(λ(x : a) → λ(xs : list) → if f x then cons x xs else xs)
)
let example0 = assert : filter Natural Natural/even [ 2, 3, 5 ] ≡ [ 2 ]
let example1 = assert : filter Natural Natural/odd [ 2, 3, 5 ] ≡ [ 3, 5 ]
in filter

4
List/filterMap.dhall
View file

@ -1,7 +1,7 @@
λ(nix : ../NixPrelude.dhall) → λ(nix : ../NixPrelude.dhall) →
let List/concatMap = ./concatMap.dhall let List/concatMap = https://prelude.dhall-lang.org/List/concatMap.dhall
let Optional/toList = ../Optional/toList.dhall nix let Optional/toList = https://prelude.dhall-lang.org/Optional/toList.dhall
let filterMap let filterMap
: ∀(a : Type) → ∀(b : Type) → (a → Optional b) → List a → List b : ∀(a : Type) → ∀(b : Type) → (a → Optional b) → List a → List b

43
List/fold.dhall
View file

@ -1,43 +0,0 @@
{-|
`fold` is the primitive function for consuming `List`s
If you treat the list `[ x, y, z ]` as `cons x (cons y (cons z nil))`, then a
`fold` just replaces each `cons` and `nil` with something else
-}
let fold
: ∀(a : Type) →
List a →
∀(list : Type) →
∀(cons : a → list → list) →
∀(nil : list) →
list
= List/fold
let example0 =
assert
: fold
Natural
[ 2, 3, 5 ]
Text
(λ(x : Natural) → λ(y : Text) → Natural/show x ++ y)
"0"
≡ "2350"
let example1 =
λ(nil : Text) →
assert
: fold
Natural
[ 2, 3, 5 ]
Text
(λ(x : Natural) → λ(y : Text) → Natural/show x ++ y)
nil
≡ "2" ++ ("3" ++ ("5" ++ nil))
let example2 =
λ(cons : Natural → Text → Text) →
λ(nil : Text) →
assert
: fold Natural [ 2, 3, 5 ] Text cons nil ≡ cons 2 (cons 3 (cons 5 nil))
in fold

60
List/foldLeft.dhall
View file

@ -1,60 +0,0 @@
{-|
`foldLeft` is like `List/fold` except that the accumulation starts from the left
If you treat the list `[ x, y, z ]` as `cons (cons (cons nil x) y) z`, then
`foldLeft` just replaces each `cons` and `nil` with something else
-}
let foldLeft
: ∀(a : Type) →
List a →
∀(list : Type) →
∀(cons : list → a → list) →
∀(nil : list) →
list
= λ(a : Type) →
λ(xs : List a) →
λ(list : Type) →
λ(cons : list → a → list) →
λ(nil : list) →
List/fold
a
xs
(list → list)
(λ(x : a) → λ(f : list → list) → λ(l : list) → f (cons l x))
(λ(l : list) → l)
nil
let example0 =
assert
: foldLeft
Natural
[ 2, 3, 5 ]
Text
(λ(x : Text) → λ(y : Natural) → x ++ Natural/show y)
"0"
≡ "0235"
let example1 =
assert
: ( λ(nil : Text) →
foldLeft
Natural
[ 2, 3, 5 ]
Text
(λ(x : Text) → λ(y : Natural) → x ++ Natural/show y)
nil
)
≡ (λ(nil : Text) → nil ++ "2" ++ "3" ++ "5")
let example2 =
assert
: ( λ(cons : Text → Natural → Text) →
λ(nil : Text) →
foldLeft Natural [ 2, 3, 5 ] Text cons nil
)
≡ ( λ(cons : Text → Natural → Text) →
λ(nil : Text) →
cons (cons (cons nil 2) 3) 5
)
in foldLeft

35
List/generate.dhall
View file

@ -1,35 +0,0 @@
{-|
Build a list by calling the supplied function on all `Natural` numbers from `0`
up to but not including the supplied `Natural` number
-}
let generate
: Natural → ∀(a : Type) → (Natural → a) → List a
= λ(n : Natural) →
λ(a : Type) →
λ(f : Natural → a) →
List/build
a
( λ(list : Type) →
λ(cons : a → list → list) →
List/fold
{ index : Natural, value : {} }
( List/indexed
{}
( List/build
{}
( λ(list : Type) →
λ(cons : {} → list → list) →
Natural/fold n list (cons {=})
)
)
)
list
(λ(x : { index : Natural, value : {} }) → cons (f x.index))
)
let example0 =
assert : generate 5 Bool Natural/even ≡ [ True, False, True, False, True ]
let example1 = assert : generate 0 Bool Natural/even ≡ ([] : List Bool)
in generate

10
List/head.dhall
View file

@ -1,10 +0,0 @@
--| Retrieve the first element of the list
let head
: ∀(a : Type) → List a → Optional a
= List/head
let example0 = assert : head Natural [ 0, 1, 2 ] ≡ Some 0
let example1 = assert : head Natural ([] : List Natural) ≡ None Natural
in head

15
List/index.dhall
View file

@ -1,15 +0,0 @@
--| Retrieve an element from a `List` using its 0-based index
let drop = ./drop.dhall
let index
: Natural → ∀(a : Type) → List a → Optional a
= λ(n : Natural) → λ(a : Type) → λ(xs : List a) → List/head a (drop n a xs)
let property =
λ(n : Natural) → λ(a : Type) → assert : index n a ([] : List a) ≡ None a
let example0 = assert : index 1 Natural [ 2, 3, 5 ] ≡ Some 3
let example1 = assert : index 1 Natural ([] : List Natural) ≡ None Natural
in index

19
List/indexed.dhall
View file

@ -1,19 +0,0 @@
--| Tag each element of the list with its index
let indexed
: ∀(a : Type) → List a → List { index : Natural, value : a }
= List/indexed
let example0 =
assert
: indexed Bool [ True, False, True ]
≡ [ { index = 0, value = True }
, { index = 1, value = False }
, { index = 2, value = True }
]
let example1 =
assert
: indexed Bool ([] : List Bool)
≡ ([] : List { index : Natural, value : Bool })
in indexed

42
List/iterate.dhall
View file

@ -1,42 +0,0 @@
{-|
Generate a list of the specified length given a seed value and transition
function
-}
let iterate
: Natural → ∀(a : Type) → (a → a) → a → List a
= λ(n : Natural) →
λ(a : Type) →
λ(f : a → a) →
λ(x : a) →
List/build
a
( λ(list : Type) →
λ(cons : a → list → list) →
List/fold
{ index : Natural, value : {} }
( List/indexed
{}
( List/build
{}
( λ(list : Type) →
λ(cons : {} → list → list) →
Natural/fold n list (cons {=})
)
)
)
list
( λ(y : { index : Natural, value : {} }) →
cons (Natural/fold y.index a f x)
)
)
let example0 =
assert
: iterate 10 Natural (λ(x : Natural) → x * 2) 1
≡ [ 1, 2, 4, 8, 16, 32, 64, 128, 256, 512 ]
let example1 =
assert
: iterate 0 Natural (λ(x : Natural) → x * 2) 1 ≡ ([] : List Natural)
in iterate

10
List/last.dhall
View file

@ -1,10 +0,0 @@
--| Retrieve the last element of the list
let last
: ∀(a : Type) → List a → Optional a
= List/last
let example0 = assert : last Natural [ 0, 1, 2 ] ≡ Some 2
let example1 = assert : last Natural ([] : List Natural) ≡ None Natural
in last

10
List/length.dhall
View file

@ -1,10 +0,0 @@
--| Returns the number of elements in a list
let length
: ∀(a : Type) → List a → Natural
= List/length
let example0 = assert : length Natural [ 0, 1, 2 ] ≡ 3
let example1 = assert : length Natural ([] : List Natural) ≡ 0
in length

23
List/map.dhall
View file

@ -1,23 +0,0 @@
--| Transform a list by applying a function to each element
let map
: ∀(a : Type) → ∀(b : Type) → (a → b) → List a → List b
= λ(a : Type) →
λ(b : Type) →
λ(f : a → b) →
λ(xs : List a) →
List/build
b
( λ(list : Type) →
λ(cons : b → list → list) →
List/fold a xs list (λ(x : a) → cons (f x))
)
let example0 =
assert
: map Natural Bool Natural/even [ 2, 3, 5 ] ≡ [ True, False, False ]
let example1 =
assert
: map Natural Bool Natural/even ([] : List Natural) ≡ ([] : List Bool)
in map

10
List/null.dhall
View file

@ -1,10 +0,0 @@
--| Returns `True` if the `List` is empty and `False` otherwise
let null
: ∀(a : Type) → List a → Bool
= λ(a : Type) → λ(xs : List a) → Natural/isZero (List/length a xs)
let example0 = assert : null Natural [ 0, 1, 2 ] ≡ False
let example1 = assert : null Natural ([] : List Natural) ≡ True
in null

31
List/package.dhall
View file

@ -1,31 +1,4 @@
λ(nix : ../NixPrelude.dhall) → λ(nix : ../NixPrelude.dhall) →
{ all = ./all.dhall {
, any = ./any.dhall , filterMap = ./filterMap.dhall
, build = ./build.dhall
, concat = ./concat.dhall
, concatMap = ./concatMap.dhall
, default = ./default.dhall nix
, drop = ./drop.dhall
, empty = ./empty.dhall
, filter = ./filter.dhall
, filterMap = ./filterMap.dhall nix
, fold = ./fold.dhall
, foldLeft = ./foldLeft.dhall
, generate = ./generate.dhall
, head = ./head.dhall
, index = ./index.dhall
, indexed = ./indexed.dhall
, iterate = ./iterate.dhall
, last = ./last.dhall
, length = ./length.dhall
, map = ./map.dhall
, null = ./null.dhall
, partition = ./partition.dhall
, replicate = ./replicate.dhall
, reverse = ./reverse.dhall
, shifted = ./shifted.dhall
, take = ./take.dhall
, unpackOptionals = ./unpackOptionals.dhall nix
, unzip = ./unzip.dhall
, zip = ./zip.dhall nix
} }

31
List/partition.dhall
View file

@ -1,31 +0,0 @@
{-|
`partition` divides a `List` of elements into those that satisfy a predicate
and those that do not
-}
let Partition
: Type → Type
= λ(a : Type) → { true : List a, false : List a }
let partition
: ∀(a : Type) → (a → Bool) → List a → Partition a
= λ(a : Type) →
λ(f : a → Bool) →
λ(xs : List a) →
List/fold
a
xs
(Partition a)
( λ(x : a) →
λ(p : Partition a) →
if f x
then { true = [ x ] # p.true, false = p.false }
else { true = p.true, false = [ x ] # p.false }
)
{ true = [] : List a, false = [] : List a }
let example0 =
assert
: partition Natural Natural/even [ 0, 1, 2, 3 ]
≡ { true = [ 0, 2 ], false = [ 1, 3 ] }
in partition

18
List/replicate.dhall
View file

@ -1,18 +0,0 @@
--| Build a list by copying the given element the specified number of times
let replicate
: Natural → ∀(a : Type) → a → List a
= λ(n : Natural) →
λ(a : Type) →
λ(x : a) →
List/build
a
( λ(list : Type) →
λ(cons : a → list → list) →
Natural/fold n list (cons x)
)
let example0 = assert : replicate 9 Natural 1 ≡ [ 1, 1, 1, 1, 1, 1, 1, 1, 1 ]
let example1 = assert : replicate 0 Natural 1 ≡ ([] : List Natural)
in replicate

11
List/reverse.dhall
View file

@ -1,11 +0,0 @@
--| Reverse a list
let reverse
: ∀(a : Type) → List a → List a
= List/reverse
let example0 = assert : reverse Natural [ 0, 1, 2 ] ≡ [ 2, 1, 0 ]
let example1 =
assert : reverse Natural ([] : List Natural) ≡ ([] : List Natural)
in reverse

83
List/shifted.dhall
View file

@ -1,83 +0,0 @@
{-|
Combine a `List` of `List`s, offsetting the `index` of each element by the
number of elements in preceding lists
-}
let shifted
: ∀(a : Type) →
List (List { index : Natural, value : a }) →
List { index : Natural, value : a }
= λ(a : Type) →
λ(kvss : List (List { index : Natural, value : a })) →
List/build
{ index : Natural, value : a }
( λ(list : Type) →
λ(cons : { index : Natural, value : a } → list → list) →
λ(nil : list) →
let result =
List/fold
(List { index : Natural, value : a })
kvss
{ count : Natural, diff : Natural → list }
( λ(kvs : List { index : Natural, value : a }) →
λ(y : { count : Natural, diff : Natural → list }) →
let length =
List/length { index : Natural, value : a } kvs
in { count = y.count + length
, diff =
λ(n : Natural) →
List/fold
{ index : Natural, value : a }
kvs
list
( λ ( kvOld
: { index : Natural, value : a }
) →
λ(z : list) →
let kvNew =
{ index = kvOld.index + n
, value = kvOld.value
}
in cons kvNew z
)
(y.diff (n + length))
}
)
{ count = 0, diff = λ(_ : Natural) → nil }
in result.diff 0
)
let example0 =
assert
: shifted
Bool
[ [ { index = 0, value = True }
, { index = 1, value = True }
, { index = 2, value = True }
]
, [ { index = 0, value = False }, { index = 1, value = False } ]
, [ { index = 0, value = True }
, { index = 1, value = True }
, { index = 2, value = True }
, { index = 3, value = True }
]
]
≡ [ { index = 0, value = True }
, { index = 1, value = True }
, { index = 2, value = True }
, { index = 3, value = False }
, { index = 4, value = False }
, { index = 5, value = True }
, { index = 6, value = True }
, { index = 7, value = True }
, { index = 8, value = True }
]
let example1 =
assert
: shifted Bool ([] : List (List { index : Natural, value : Bool }))
≡ ([] : List { index : Natural, value : Bool })
in shifted

23
List/take.dhall
View file

@ -1,23 +0,0 @@
--| Truncate a list to the first `n` elements
let Natural/lessThan = ../Natural/lessThan.dhall
let take
: ∀(n : Natural) → ∀(a : Type) → List a → List a
= λ(n : Natural) →
λ(a : Type) →
λ(xs : List a) →
List/fold
{ index : Natural, value : a }
(List/indexed a xs)
(List a)
( λ(x : { index : Natural, value : a }) →
λ(xs : List a) →
if Natural/lessThan x.index n then [ x.value ] # xs else xs
)
([] : List a)
let example = assert : take 2 Natural [ 2, 3, 5 ] ≡ [ 2, 3 ]
let example = assert : take 5 Natural [ 2, 3, 5 ] ≡ [ 2, 3, 5 ]
in take

8
List/unpackOptionals.dhall
View file

@ -1,8 +0,0 @@
λ(nix : ../NixPrelude.dhall) →
let List/filterMap = ./filterMap.dhall nix
let unpackOptionals
: ∀(a : Type) → ∀(l : List (Optional a)) → List a
= λ(a : Type) → List/filterMap (Optional a) a (λ(x : Optional a) → x)
in unpackOptionals

50
List/unzip.dhall
View file

@ -1,50 +0,0 @@
--| Unzip a `List` into two separate `List`s
let unzip
: ∀(a : Type) →
∀(b : Type) →
List { _1 : a, _2 : b } →
{ _1 : List a, _2 : List b }
= λ(a : Type) →
λ(b : Type) →
λ(xs : List { _1 : a, _2 : b }) →
{ _1 =
List/build
a
( λ(list : Type) →
λ(cons : a → list → list) →
List/fold
{ _1 : a, _2 : b }
xs
list
(λ(x : { _1 : a, _2 : b }) → cons x._1)
)
, _2 =
List/build
b
( λ(list : Type) →
λ(cons : b → list → list) →
List/fold
{ _1 : a, _2 : b }
xs
list
(λ(x : { _1 : a, _2 : b }) → cons x._2)
)
}
let example0 =
assert
: unzip
Text
Bool
[ { _1 = "ABC", _2 = True }
, { _1 = "DEF", _2 = False }
, { _1 = "GHI", _2 = True }
]
≡ { _1 = [ "ABC", "DEF", "GHI" ], _2 = [ True, False, True ] }
let example1 =
assert
: unzip Text Bool ([] : List { _1 : Text, _2 : Bool })
≡ { _1 = [] : List Text, _2 = [] : List Bool }
in unzip

36
List/zip.dhall
View file

@ -1,36 +0,0 @@
λ(nix : ../NixPrelude.dhall) →
let List/index = ./index.dhall
let List/map = ./map.dhall
let Natural/min = ../Natural/min.dhall
let Natural/enumerate = ../Natural/enumerate.dhall
let Optional/unwrap = ../Optional/unwrap.dhall nix
let zip
: ∀(a : Type) → List a → ∀(b : Type) → List b → List { _1 : a, _2 : b }
= λ(a : Type) →
λ(xs : List a) →
λ(b : Type) →
λ(ys : List b) →
let xsLen = List/length a xs
let ysLen = List/length b ys
let resLen = Natural/min xsLen ysLen
let indexes = Natural/enumerate resLen
in List/map
Natural
{ _1 : a, _2 : b }
( λ(i : Natural) →
{ _1 = Optional/unwrap a (List/index i a xs)
, _2 = Optional/unwrap b (List/index i b ys)
}
)
indexes
in zip

15
Location/Type.dhall
View file

@ -1,15 +0,0 @@
--| This is the union type returned when you import something `as Location`
let Location
: Type
= < Environment : Text | Local : Text | Missing | Remote : Text >
let example0 =
assert
: missing as Location
≡ < Environment : Text
| Local : Text
| Missing
| Remote : Text
>.Missing
in Location

1
Location/package.dhall
View file

@ -1 +0,0 @@
{ Type = ./Type.dhall }

6
Map/Entry.dhall
View file

@ -1,6 +0,0 @@
--| The type of each key-value pair in a `Map`
let Entry
: Type → Type → Type
= λ(k : Type) → λ(v : Type) → { mapKey : k, mapValue : v }
in Entry

25
Map/Type.dhall
View file

@ -1,25 +0,0 @@
{-|
This is the canonical way to encode a dynamic list of key-value pairs.
Tools (such as `dhall-to-json`/`dhall-to-yaml` will recognize values of this
type and convert them to maps/dictionaries/hashes in the target language
For example, `dhall-to-json` converts a Dhall value like this:
```
[ { mapKey = "foo", mapValue = 1 }
, { mapKey = "bar", mapValue = 2 }
] : ./Map Text Natural
```
... to a JSON value like this:
```
{ "foo": 1, "bar", 2 }
```
-}
let Map
: Type → Type → Type
= λ(k : Type) → λ(v : Type) → List { mapKey : k, mapValue : v }
in Map

11
Map/empty.dhall
View file

@ -1,11 +0,0 @@
--| An empty `Map` of the given key and value types
let Map = ./Type.dhall
let empty
: ∀(k : Type) → ∀(v : Type) → Map k v
= λ(k : Type) → λ(v : Type) → [] : Map k v
let example0 =
assert : empty Text Bool ≡ ([] : List { mapKey : Text, mapValue : Bool })
in empty

15
Map/keyText.dhall
View file

@ -1,15 +0,0 @@
{-|
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 `./keyValue` for a polymorphic version.
-}
let keyText =
λ(key : Text) → λ(value : Text) → { mapKey = key, mapValue = value }
let example0 =
assert : keyText "foo" "bar" ≡ { mapKey = "foo", mapValue = "bar" }
in keyText

Some files were not shown because too many files have changed in this diff Show more