Initial Dhall functions

Add functions for representing the JSON subset of Preserves in the
Dhall configuration language.

https://dhall-lang.org/

implementations/README.md

@@ -2,6 +2,9 @@
 
 Here you may find:
 
+ - [dhall](dhall/), functions for converting Dhall values to a corresponding
+   subset of Preserves.
+
  - [javascript](javascript/), an implementation in TypeScript,
    compiling to JavaScript, for node.js and the Browser.
 

implementations/dhall/Prelude.dhall

@@ -0,0 +1,3 @@
+  env:DHALL_PRELUDE
+? https://prelude.dhall-lang.org/v20.2.0/package.dhall
+    sha256:a6036bc38d883450598d1de7c98ead113196fe2db02e9733855668b18096f07b

implementations/dhall/README.md

@@ -0,0 +1,48 @@
+# Dhall
+
+Not a true implementation of Preserves, but functions for translating Dhall
+values to Preserves and rendering them.
+
+For example, to generate configuration for a Syndicate server listener:
+```dhall
+let Prelude = ./Prelude.dhall
+
+let Preserves = ./package.dhall
+
+let Tcp/Type = { address : Text, port : Natural }
+
+let RelayListener/Type = { transport : Tcp/Type }
+
+let RequireService/Type = { relayListener : RelayListener/Type }
+
+let Tcp/toPreserves =
+      λ(tcp : Tcp/Type) →
+        Preserves.record
+          (Preserves.symbol "tcp")
+          [ Preserves.string tcp.address
+          , Preserves.integer (Prelude.Natural.toInteger tcp.port)
+          ]
+
+let RelayListener/toPreserves =
+      λ(relayListener : RelayListener/Type) →
+        Preserves.record
+          (Preserves.symbol "relay-listener")
+          [ Tcp.toPreserves relayListener.transport ]
+
+let RequireService/toPreserves =
+      λ(requireService : RequireService/Type) →
+        Preserves.record
+          (Preserves.symbol "require-service")
+          [ RelayListener.toPreserves requireService.relayListener ]
+
+let example = { relayListener.transport = { address = "127.0.0.1", port = 1 } }
+
+let rendering = Preserves.render (RequireService.toPreserves example)
+
+let check =
+        assert
+      : rendering ≡ "<require-service <relay-listener <tcp \"127.0.0.1\" 1>>>"
+
+in  rendering
+
+```

implementations/dhall/Type.dhall

@@ -0,0 +1,10 @@
+{-|
+Dhall encoding of an arbitrary Preserves value
+-}
+let Preserves/function = ./function.dhall
+
+let Preserves/Type
+    : Type
+    = ∀(Preserves : Type) → ∀(value : Preserves/function Preserves) → Preserves
+
+in  Preserves/Type

implementations/dhall/boolean.dhall

@@ -0,0 +1,15 @@
+{-|
+Create a Preserves boolean map from a `Bool` value
+-}
+let Preserves/Type = ./Type.dhall
+
+let Preserves/function = ./function.dhall
+
+let bool
+    : Bool → Preserves/Type
+    = λ(x : Bool) →
+      λ(Preserves : Type) →
+      λ(value : Preserves/function Preserves) →
+        value.boolean x
+
+in  bool

implementations/dhall/dictionary.dhall

@@ -0,0 +1,37 @@
+{-|
+Create a Preserves dictionary value from a Dhall `Map` of `Preserves` values
+-}
+let Prelude = ./Prelude.dhall
+
+let List/map = Prelude.List.map
+
+let Map/Entry = Prelude.Map.Entry
+
+let Preserves = ./Type.dhall
+
+let Preserves/function = ./function.dhall
+
+let Preserves/Entry = Map/Entry Preserves Preserves
+
+let Preserves/Map = List Preserves/Entry
+
+let map
+    : Preserves/Map → Preserves
+    = λ(x : Preserves/Map) →
+      λ(Preserves : Type) →
+        let Preserves/Entry = Map/Entry Preserves Preserves
+
+        in  λ(value : Preserves/function Preserves) →
+              value.dictionary
+                ( List/map
+                    Preserves/Entry@1
+                    Preserves/Entry
+                    ( λ(e : Preserves/Entry@1) →
+                        { mapKey = e.mapKey Preserves value
+                        , mapValue = e.mapValue Preserves value
+                        }
+                    )
+                    x
+                )
+
+in  map

implementations/dhall/dictionaryOf.dhall

@@ -0,0 +1,40 @@
+{-|
+Create a Preserves dictionary value from a Dhall `Map`
+
+See ./render.dhall for an example.
+-}
+let Prelude = ./Prelude.dhall
+
+let List/map = Prelude.List.map
+
+let Preserves = ./Type.dhall
+
+let Preserves/dictionary = ./dictionary.dhall
+
+let dictionaryOf
+    : ∀(a : Type) →
+      (a → Preserves) →
+      ∀(b : Type) →
+      (b → Preserves) →
+      Prelude.Map.Type a b →
+        Preserves
+    = λ(a : Type) →
+      λ(key : a → Preserves) →
+      λ(b : Type) →
+      λ(value : b → Preserves) →
+      λ(x : Prelude.Map.Type a b) →
+        let ab = Prelude.Map.Entry a b
+
+        let pp = Prelude.Map.Entry Preserves Preserves
+
+        in  Preserves/dictionary
+              ( List/map
+                  ab
+                  pp
+                  ( λ(x : ab) →
+                      { mapKey = key x.mapKey, mapValue = value x.mapValue }
+                  )
+                  x
+              )
+
+in  dictionaryOf

implementations/dhall/double.dhall

@@ -0,0 +1,15 @@
+{-|
+Create a Preserves floating-point value from a `Double` value
+-}
+let Preserves = ./Type.dhall
+
+let Preserves/function = ./function.dhall
+
+let double
+    : Double → Preserves
+    = λ(x : Double) →
+      λ(Preserves : Type) →
+      λ(value : Preserves/function Preserves) →
+        value.double x
+
+in  double

implementations/dhall/embedded.dhall

@@ -0,0 +1,15 @@
+{-|
+Create an embedded Preserves value.
+-}
+let Preserves = ./Type.dhall
+
+let Preserves/function = ./function.dhall
+
+let embedded
+    : Preserves → Preserves
+    = λ(value : Preserves) →
+      λ(Preserves : Type) →
+      λ(value : Preserves/function Preserves) →
+        value.embedded (value@1 Preserves value)
+
+in  embedded

implementations/dhall/fromJSON.dhall

@@ -0,0 +1,40 @@
+{-|
+Translate a `JSON` value to a `Preserves` value
+-}
+let Prelude = ./Prelude.dhall
+
+let List/map = Prelude.List.map
+
+let JSON = Prelude.JSON.Type
+
+let Preserves = ./Type.dhall
+
+let Preserves/function = ./function.dhall
+
+let fromJSON
+    : JSON → Preserves
+    = λ(json : JSON) →
+      λ(Preserves : Type) →
+      λ(value : Preserves/function Preserves) →
+        json
+          Preserves
+          { array = value.sequence
+          , bool = λ(x : Bool) → value.symbol (if x then "true" else "false")
+          , double = value.double
+          , integer = value.integer
+          , null = value.symbol "null"
+          , object =
+              let Entry = { mapKey : Text, mapValue : Preserves }
+
+              in  λ(m : List Entry) →
+                    value.dictionary
+                      ( List/map
+                          Entry
+                          { mapKey : Preserves, mapValue : Preserves }
+                          (λ(e : Entry) → e with mapKey = value.string e.mapKey)
+                          m
+                      )
+          , string = value.string
+          }
+
+in  fromJSON

implementations/dhall/function.dhall

@@ -0,0 +1,12 @@
+λ(Preserves : Type) →
+  { boolean : Bool → Preserves
+  , double : Double → Preserves
+  , integer : Integer → Preserves
+  , string : Text → Preserves
+  , symbol : Text → Preserves
+  , record : Preserves → List Preserves → Preserves
+  , sequence : List Preserves → Preserves
+  , set : List Preserves → Preserves
+  , dictionary : List { mapKey : Preserves, mapValue : Preserves } → Preserves
+  , embedded : Preserves → Preserves
+  }

implementations/dhall/integer.dhall

@@ -0,0 +1,15 @@
+{-|
+Create a Preserves integer value from an `Integer` value
+-}
+let Preserves = ./Type.dhall
+
+let Preserves/function = ./function.dhall
+
+let integer
+    : Integer → Preserves
+    = λ(x : Integer) →
+      λ(Preserves : Type) →
+      λ(value : Preserves/function Preserves) →
+        value.integer x
+
+in  integer

implementations/dhall/package.dhall

@@ -0,0 +1,16 @@
+{ Type = ./Type.dhall
+, function = ./function.dhall
+, boolean = ./boolean.dhall
+, dictionary = ./dictionary.dhall
+, dictionaryOf = ./dictionaryOf.dhall
+, double = ./double.dhall
+, embedded = ./embedded.dhall
+, fromJSON = ./fromJSON.dhall
+, integer = ./integer.dhall
+, record = ./record.dhall
+, render = ./render.dhall
+, sequence = ./sequence.dhall
+, sequenceOf = ./sequenceOf.dhall
+, string = ./string.dhall
+, symbol = ./symbol.dhall
+}

implementations/dhall/record.dhall

@@ -0,0 +1,23 @@
+let Prelude = ./Prelude.dhall
+
+let List/map = Prelude.List.map
+
+let Preserves = ./Type.dhall
+
+let Preserves/function = ./function.dhall
+
+let record =
+      λ(label : Preserves) →
+      λ(fields : List Preserves) →
+      λ(Preserves : Type) →
+      λ(value : Preserves/function Preserves) →
+        value.record
+          (label Preserves value)
+          ( List/map
+              Preserves@1
+              Preserves
+              (λ(value : Preserves@1) → value Preserves value@1)
+              fields
+          )
+
+in  record

implementations/dhall/render.dhall

@@ -0,0 +1,100 @@
+{-
+Render a `Preserves` value to a diagnostic `Text` value
+-}
+let Preserves = ./Type.dhall
+
+let Prelude = ./Prelude.dhall
+
+let Map/Type = Prelude.Map.Type
+
+let Text/concatSep = Prelude.Text.concatSep
+
+let Text/concatMapSep = Prelude.Text.concatMapSep
+
+let render
+    : Preserves → Text
+    = λ(value : Preserves) →
+        value
+          Text
+          { boolean = λ(x : Bool) → if x then "#t" else "#f"
+          , double = Double/show
+          , integer = Prelude.JSON.renderInteger
+          , string = Text/show
+          , symbol = λ(sym : Text) → "${sym}"
+          , record =
+              λ(label : Text) →
+              λ(fields : List Text) →
+                    "<${label}"
+                ++  (if Prelude.List.null Text fields then "" else " ")
+                ++  Text/concatSep " " fields
+                ++  ">"
+          , sequence = λ(xs : List Text) → "[ " ++ Text/concatSep " " xs ++ " ]"
+          , set = λ(xs : List Text) → "#{" ++ Text/concatSep " " xs ++ " }"
+          , dictionary =
+              λ(m : Map/Type Text Text) →
+                    "{ "
+                ++  Text/concatMapSep
+                      " "
+                      { mapKey : Text, mapValue : Text }
+                      ( λ(e : { mapKey : Text, mapValue : Text }) →
+                          "${e.mapKey}: ${e.mapValue}"
+                      )
+                      m
+                ++  " }"
+          , embedded = λ(value : Text) → "#!${value}"
+          }
+
+let Preserves/boolean = ./boolean.dhall
+
+let Preserves/integer = ./integer.dhall
+
+let Preserves/double = ./double.dhall
+
+let Preserves/symbol = ./symbol.dhall
+
+let Preserves/record = ./record.dhall
+
+let Preserves/sequenceOf = ./sequenceOf.dhall
+
+let Preserves/dictionaryOf = ./dictionaryOf.dhall
+
+let Preserves/dictionaryOfSymbols = Preserves/dictionaryOf Text Preserves/symbol
+
+let Preserves/embedded = ./embedded.dhall
+
+let example0 =
+        assert
+      :   ''
+          ${render
+              ( Preserves/dictionaryOfSymbols
+                  Preserves
+                  (λ(x : Preserves) → x)
+                  ( toMap
+                      { a = Preserves/integer +1
+                      , b =
+                          Preserves/sequenceOf
+                            Integer
+                            Preserves/integer
+                            [ +2, +3 ]
+                      , c =
+                          Preserves/dictionaryOfSymbols
+                            Double
+                            Preserves/double
+                            (toMap { d = 1.0, e = -1.0 })
+                      , d = Preserves/embedded (Preserves/boolean True)
+                      , e =
+                          Preserves/record
+                            (Preserves/symbol "capture")
+                            [ Preserves/record
+                                (Preserves/symbol "_")
+                                ([] : List Preserves)
+                            ]
+                      }
+                  )
+              )}
+          ''
+        ≡ ''
+          { a: 1 b: [ 2 3 ] c: { d: 1.0 e: -1.0 } d: #!#t e: <capture <_>> }
+          ''
+
+in  render

implementations/dhall/sequence.dhall

@@ -0,0 +1,27 @@
+{-|
+Create a Preserves sequence value from a `List` of `Preserve` values
+
+See ./sequenceOf.dhall for an example.
+-}
+let Prelude = ./Prelude.dhall
+
+let List/map = Prelude.List.map
+
+let Preserves = ./Type.dhall
+
+let Preserves/function = ./function.dhall
+
+let sequence
+    : List Preserves → Preserves
+    = λ(x : List Preserves) →
+      λ(Preserves : Type) →
+      λ(value : Preserves/function Preserves) →
+        value.sequence
+          ( List/map
+              Preserves@1
+              Preserves
+              (λ(value : Preserves@1) → value Preserves value@1)
+              x
+          )
+
+in  sequence

implementations/dhall/sequenceOf.dhall

@@ -0,0 +1,21 @@
+{-|
+Create a Preserves sequence value from a `List` of values and a conversion function
+
+See ./render.dhall for an example.
+-}
+let Prelude = ./Prelude.dhall
+
+let List/map = Prelude.List.map
+
+let Preserves = ./Type.dhall
+
+let Preserves/sequence = ./sequence.dhall
+
+let sequenceOf
+    : ∀(a : Type) → (a → Preserves) → List a → Preserves
+    = λ(a : Type) →
+      λ(f : a → Preserves) →
+      λ(xs : List a) →
+        Preserves/sequence (List/map a Preserves f xs)
+
+in  sequenceOf

implementations/dhall/string.dhall

@@ -0,0 +1,15 @@
+{-|
+Create a Preserves string from a `Text` value
+-}
+let Preserves/Type = ./Type.dhall
+
+let Preserves/function = ./function.dhall
+
+let string
+    : Text → Preserves/Type
+    = λ(x : Text) →
+      λ(Preserves : Type) →
+      λ(value : Preserves/function Preserves) →
+        value.string x
+
+in  string

implementations/dhall/symbol.dhall

@@ -0,0 +1,15 @@
+{-|
+Create a Preserves symbol from a `Text` value
+-}
+let Preserves/Type = ./Type.dhall
+
+let Preserves/function = ./function.dhall
+
+let symbol
+    : Text → Preserves/Type
+    = λ(x : Text) →
+      λ(Preserves : Type) →
+      λ(value : Preserves/function Preserves) →
+        value.symbol x
+
+in  symbol