From 2ff489d9753169ef57446d22cfd4722ca1264e2e Mon Sep 17 00:00:00 2001 From: Emery Hemingway Date: Fri, 22 Oct 2021 12:40:11 +0200 Subject: [PATCH] Initial Dhall functions Add functions for representing the JSON subset of Preserves in the Dhall configuration language. https://dhall-lang.org/ --- implementations/README.md | 3 + implementations/dhall/Prelude.dhall | 3 + implementations/dhall/README.md | 48 +++++++++++ implementations/dhall/Type.dhall | 10 +++ implementations/dhall/boolean.dhall | 15 ++++ implementations/dhall/dictionary.dhall | 37 +++++++++ implementations/dhall/dictionaryOf.dhall | 40 +++++++++ implementations/dhall/double.dhall | 15 ++++ implementations/dhall/embedded.dhall | 15 ++++ implementations/dhall/fromJSON.dhall | 40 +++++++++ implementations/dhall/function.dhall | 12 +++ implementations/dhall/integer.dhall | 15 ++++ implementations/dhall/package.dhall | 16 ++++ implementations/dhall/record.dhall | 23 ++++++ implementations/dhall/render.dhall | 100 +++++++++++++++++++++++ implementations/dhall/sequence.dhall | 27 ++++++ implementations/dhall/sequenceOf.dhall | 21 +++++ implementations/dhall/string.dhall | 15 ++++ implementations/dhall/symbol.dhall | 15 ++++ 19 files changed, 470 insertions(+) create mode 100644 implementations/dhall/Prelude.dhall create mode 100644 implementations/dhall/README.md create mode 100644 implementations/dhall/Type.dhall create mode 100644 implementations/dhall/boolean.dhall create mode 100644 implementations/dhall/dictionary.dhall create mode 100644 implementations/dhall/dictionaryOf.dhall create mode 100644 implementations/dhall/double.dhall create mode 100644 implementations/dhall/embedded.dhall create mode 100644 implementations/dhall/fromJSON.dhall create mode 100644 implementations/dhall/function.dhall create mode 100644 implementations/dhall/integer.dhall create mode 100644 implementations/dhall/package.dhall create mode 100644 implementations/dhall/record.dhall create mode 100644 implementations/dhall/render.dhall create mode 100644 implementations/dhall/sequence.dhall create mode 100644 implementations/dhall/sequenceOf.dhall create mode 100644 implementations/dhall/string.dhall create mode 100644 implementations/dhall/symbol.dhall diff --git a/implementations/README.md b/implementations/README.md index 59cb04e..c0d0399 100644 --- a/implementations/README.md +++ b/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. diff --git a/implementations/dhall/Prelude.dhall b/implementations/dhall/Prelude.dhall new file mode 100644 index 0000000..034dfb5 --- /dev/null +++ b/implementations/dhall/Prelude.dhall @@ -0,0 +1,3 @@ + env:DHALL_PRELUDE +? https://prelude.dhall-lang.org/v20.2.0/package.dhall + sha256:a6036bc38d883450598d1de7c98ead113196fe2db02e9733855668b18096f07b diff --git a/implementations/dhall/README.md b/implementations/dhall/README.md new file mode 100644 index 0000000..84d931e --- /dev/null +++ b/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 ≡ ">>" + +in rendering + +``` diff --git a/implementations/dhall/Type.dhall b/implementations/dhall/Type.dhall new file mode 100644 index 0000000..4a606db --- /dev/null +++ b/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 diff --git a/implementations/dhall/boolean.dhall b/implementations/dhall/boolean.dhall new file mode 100644 index 0000000..ade2d62 --- /dev/null +++ b/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 diff --git a/implementations/dhall/dictionary.dhall b/implementations/dhall/dictionary.dhall new file mode 100644 index 0000000..f8c02d9 --- /dev/null +++ b/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 diff --git a/implementations/dhall/dictionaryOf.dhall b/implementations/dhall/dictionaryOf.dhall new file mode 100644 index 0000000..78f59a6 --- /dev/null +++ b/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 diff --git a/implementations/dhall/double.dhall b/implementations/dhall/double.dhall new file mode 100644 index 0000000..6e2b5dc --- /dev/null +++ b/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 diff --git a/implementations/dhall/embedded.dhall b/implementations/dhall/embedded.dhall new file mode 100644 index 0000000..dde92b2 --- /dev/null +++ b/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 diff --git a/implementations/dhall/fromJSON.dhall b/implementations/dhall/fromJSON.dhall new file mode 100644 index 0000000..3bc90ab --- /dev/null +++ b/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 diff --git a/implementations/dhall/function.dhall b/implementations/dhall/function.dhall new file mode 100644 index 0000000..1226db6 --- /dev/null +++ b/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 + } diff --git a/implementations/dhall/integer.dhall b/implementations/dhall/integer.dhall new file mode 100644 index 0000000..88ca3fb --- /dev/null +++ b/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 diff --git a/implementations/dhall/package.dhall b/implementations/dhall/package.dhall new file mode 100644 index 0000000..25a8316 --- /dev/null +++ b/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 +} diff --git a/implementations/dhall/record.dhall b/implementations/dhall/record.dhall new file mode 100644 index 0000000..a9c5cca --- /dev/null +++ b/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 diff --git a/implementations/dhall/render.dhall b/implementations/dhall/render.dhall new file mode 100644 index 0000000..e05db05 --- /dev/null +++ b/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: > } + '' + +in render diff --git a/implementations/dhall/sequence.dhall b/implementations/dhall/sequence.dhall new file mode 100644 index 0000000..413efdb --- /dev/null +++ b/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 diff --git a/implementations/dhall/sequenceOf.dhall b/implementations/dhall/sequenceOf.dhall new file mode 100644 index 0000000..49e7400 --- /dev/null +++ b/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 diff --git a/implementations/dhall/string.dhall b/implementations/dhall/string.dhall new file mode 100644 index 0000000..8507690 --- /dev/null +++ b/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 diff --git a/implementations/dhall/symbol.dhall b/implementations/dhall/symbol.dhall new file mode 100644 index 0000000..e35079b --- /dev/null +++ b/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