Profpatsch/document-stdlib.sh

## document-stdlib.sh
#!/usr/bin/env nix-shell
#!nix-shell -i bash -p bash -p lr -p pandoc

set -euo pipefail

preludeDir="${1:?dir please}"

# each file (except package.dhall) starts with a multiline-comment with markdown docstrings.
# {- maybe docstring
# docstring
# maybe docstring -}
parseDocstringForFile () {
    local doc=$(sed -n \
                    -e '/^{-/,/-}$/ p' \
                    "$1" \
                    | sed -e '1s/^{-\s*//' \
                    | sed -e '$s/\s*-}$//')
    if [ "$doc" = "" ]; then
        printf 'WARNING: %s has no docstring\n' "$1" >&2
    fi
    printf '%s' "$doc"
}


tmp=$(mktemp -d)

for file in $(lr -t "type = f" -s "$preludeDir" "$preludeDir"); do
    # those are the export files
    if [ "$(basename "$file")" = "package.dhall" ]; then
           continue
    fi
    # printf '%s\n' "$tmp/$file"
    echo "## $file"
    echo
    parseDocstringForFile "$preludeDir/$file"
    echo
    # TODO: build helper dhall executable that can print
    # the type of expressions while caching all imports.
    # (use dhall-flycheck code for that)
    echo
    echo "### Type"
    echo '```'
    (
        # don’t use the cache to preserve variable names
        export XDG_CACHE_HOME=/var/empty
        printf '(./%spackage.dhall).%s\n' "$preludeDir" "${file/\//.}" \
            | dhall resolve \
            | dhall type
    )
    echo '```'
    echo
    echo "<hr>"
done | pandoc --standalone --to=html5

## out.html

<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml" lang="" xml:lang="">
<head>
  <meta charset="utf-8" />
  <meta name="generator" content="pandoc" />
  <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
  <title>Untitled</title>
  <style>
      code{white-space: pre-wrap;}
      span.smallcaps{font-variant: small-caps;}
      span.underline{text-decoration: underline;}
      div.column{display: inline-block; vertical-align: top; width: 50%;}
  </style>
  <!--[if lt IE 9]>
    <script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
  <![endif]-->
</head>
<body>
<h2 id="booland">Bool/and</h2>
<p>The <code>and</code> function returns <code>False</code> if there are any <code>False</code> elements in the <code>List</code> and returns <code>True</code> otherwise</p>
<h3 id="type">Type</h3>
<pre><code>∀(xs : List Bool) → Bool</code></pre>
<hr>
<h2 id="boolbuild">Bool/build</h2>
<p><code>build</code> is the inverse of <code>fold</code></p>
<h3 id="type-1">Type</h3>
<pre><code>∀(f : ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool) → Bool</code></pre>
<hr>
<h2 id="booleven">Bool/even</h2>
<p>Returns <code>True</code> if there are an even number of <code>False</code> elements in the list and returns <code>False</code> otherwise.</p>
<p>This function is the <code>Monoid</code> for the <code>==</code> operation.</p>
<h3 id="type-2">Type</h3>
<pre><code>∀(xs : List Bool) → Bool</code></pre>
<hr>
<h2 id="boolfold">Bool/fold</h2>
<p><code>fold</code> is essentially the same as <code>if</code>/<code>then</code>/else` except as a function</p>
<h3 id="type-3">Type</h3>
<pre><code>∀(b : Bool) → ∀(bool : Type) → ∀(true : bool) → ∀(false : bool) → bool</code></pre>
<hr>
<h2 id="boolnot">Bool/not</h2>
<p>Flip the value of a <code>Bool</code></p>
<h3 id="type-4">Type</h3>
<pre><code>∀(b : Bool) → Bool</code></pre>
<hr>
<h2 id="boolodd">Bool/odd</h2>
<p>Returns <code>True</code> if there are an odd number of <code>True</code> elements in the list and returns <code>False</code> otherwise.</p>
<p>This function is the <code>Monoid</code> for the <code>!=</code> operation.</p>
<h3 id="type-5">Type</h3>
<pre><code>∀(xs : List Bool) → Bool</code></pre>
<hr>
<h2 id="boolor">Bool/or</h2>
<p>The <code>or</code> function returns <code>True</code> if there are any <code>True</code> elements in the <code>List</code> and returns <code>False</code> otherwise</p>
<h3 id="type-6">Type</h3>
<pre><code>∀(xs : List Bool) → Bool</code></pre>
<hr>
<h2 id="boolshow">Bool/show</h2>
<p>Render a <code>Bool</code> as <code>Text</code> using the same representation as Dhall source code (i.e. beginning with a capital letter)</p>
<h3 id="type-7">Type</h3>
<pre><code>∀(b : Bool) → Text</code></pre>
<hr>
<h2 id="doubleshow">Double/show</h2>
<p>Render a <code>Double</code> as <code>Text</code> using the same representation as Dhall source code (i.e. a decimal floating point number with a leading <code>-</code> sign if negative)</p>
<h3 id="type-8">Type</h3>
<pre><code>Double → Text</code></pre>
<hr>
<h2 id="functioncompose">Function/compose</h2>
<p>Compose two functions into one.</p>
<h3 id="type-9">Type</h3>
<pre><code>  ∀(A : Type)
→ ∀(B : Type)
→ ∀(C : Type)
→ ∀(f : A → B)
→ ∀(g : B → C)
→ ∀(x : A)
→ C</code></pre>
<hr>
<h2 id="integershow">Integer/show</h2>
<p>Render an <code>Integer</code> as <code>Text</code> using the same representation as Dhall source code (i.e. a decimal number with a leading <code>-</code> sign if negative and a leading <code>+</code> sign if non-negative)</p>
<h3 id="type-10">Type</h3>
<pre><code>Integer → Text</code></pre>
<hr>
<h2 id="integertodouble">Integer/toDouble</h2>
<p>Convert an <code>Integer</code> to the corresponding <code>Double</code></p>
<h3 id="type-11">Type</h3>
<pre><code>Integer → Double</code></pre>
<hr>
<h2 id="jsonnesting">JSON/Nesting</h2>
<p>This type is used as part of <code>dhall-json</code>’s support for preserving alternative names</p>
<p>For example, this Dhall code:</p>
<pre><code>let Example = &lt; Left : { foo : Natural } | Right : { bar : Bool } &gt;

let Nesting = &lt; Inline | Nested : Text &gt;

in  { field =
        &quot;name&quot;
    , nesting =
        Nesting.Inline
    , contents =
        Example.Left { foo = 2 }
    }</code></pre>
<p>… generates this JSON:</p>
<pre><code>{
  &quot;foo&quot;: 2,
  &quot;name&quot;: &quot;Left&quot;
 }</code></pre>
<h3 id="type-12">Type</h3>
<pre><code>Type</code></pre>
<hr>
<h2 id="jsontagged">JSON/Tagged</h2>
<p>This is a convenient type-level function when using <code>dhall-to-json</code>’s support for preserving alternative names</p>
<p>For example, this code:</p>
<pre><code>let map = ../List/map

let Provisioner =
      &lt; shell :
          { inline : List Text }
      | file :
          { source : Text, destination : Text }
      &gt;

let Tagged = ./Tagged

let Nesting = ./Nesting

let wrap
    : Provisioner → Tagged Provisioner
    =   λ(x : Provisioner)
      → { field = &quot;type&quot;, nesting = Nesting.Nested &quot;params&quot;, contents = x }

in  { provisioners =
        map
        Provisioner
        (Tagged Provisioner)
        wrap
        [ Provisioner.shell { inline = [ &quot;echo foo&quot; ] }
        , Provisioner.file
          { source = &quot;app.tar.gz&quot;, destination = &quot;/tmp/app.tar.gz&quot; }
        ]
    }</code></pre>
<p>… produces this JSON:</p>
<pre><code>{
  &quot;provisioners&quot;: [
    {
      &quot;params&quot;: {
        &quot;inline&quot;: [
          &quot;echo foo&quot;
        ]
      },
      &quot;type&quot;: &quot;shell&quot;
    },
    {
      &quot;params&quot;: {
        &quot;destination&quot;: &quot;/tmp/app.tar.gz&quot;,
        &quot;source&quot;: &quot;app.tar.gz&quot;
      },
      &quot;type&quot;: &quot;file&quot;
    }
  ]
}</code></pre>
<h3 id="type-13">Type</h3>
<pre><code>∀(a : Type) → Type</code></pre>
<hr>
<h2 id="jsontype">JSON/Type</h2>
<p>Dhall encoding of an arbitrary JSON value</p>
<p>For example, the following JSON value:</p>
<pre><code>[ { &quot;foo&quot;: null, &quot;bar&quot;: [ 1.0, true ] } ]</code></pre>
<p>… corresponds to the following Dhall expression:</p>
<pre><code>  λ(JSON : Type)
→ λ ( json
    : { array :
          List JSON → JSON
      , bool :
          Bool → JSON
      , null :
          JSON
      , number :
          Double → JSON
      , object :
          List { mapKey : Text, mapValue : JSON } → JSON
      , string :
          Text → JSON
      }
    )
→ json.object
  [ { mapKey = &quot;foo&quot;, mapValue = json.null }
  , { mapKey =
        &quot;bar&quot;
    , mapValue =
        json.array [ json.number 1.0, json.bool True ]
    }
  ]</code></pre>
<p>You do not need to create these values directly, though. You can use the utilities exported by <code>./package.dhall</code> to create values of this type, such as:</p>
<pre><code>let JSON = ./package.dhall

in  JSON.object
    [ { mapKey = &quot;foo&quot;, mapValue = JSON.null }
    , { mapKey =
          &quot;bar&quot;
      , mapValue =
          JSON.array [ JSON.number 1.0, JSON.bool True ]
      }
    ]</code></pre>
<h3 id="type-14">Type</h3>
<pre><code>Type</code></pre>
<hr>
<h2 id="jsonarray">JSON/array</h2>
<p>Create a JSON array from a <code>List</code> of JSON values</p>
<pre><code>let JSON = ./package.dhall
in  JSON.render (JSON.array [ JSON.number 1.0, JSON.bool True ])
= &quot;[ 1.0, true ]&quot;

let JSON/Type = ./Type
let JSON = ./package.dhall
in  JSON.render (JSON.array ([] : List JSON/Type))
= &quot;[ ]&quot;</code></pre>
<h3 id="type-15">Type</h3>
<pre><code>  ∀ ( x
    : List
        (   ∀(JSON : Type)
          → ∀ ( json
              : { array : List JSON → JSON
                , bool : Bool → JSON
                , null : JSON
                , number : Double → JSON
                , object : List { mapKey : Text, mapValue : JSON } → JSON
                , string : Text → JSON
                }
              )
          → JSON
        )
    )
→ ∀(JSON : Type)
→ ∀ ( json
    : { array : List JSON → JSON
      , bool : Bool → JSON
      , null : JSON
      , number : Double → JSON
      , object : List { mapKey : Text, mapValue : JSON } → JSON
      , string : Text → JSON
      }
    )
→ JSON</code></pre>
<hr>
<h2 id="jsonbool">JSON/bool</h2>
<p>Create a JSON bool from a Dhall <code>Bool</code></p>
<pre><code>let JSON = ./package.dhall
in  JSON.render (JSON.bool True)
= &quot;true&quot;

let JSON = ./package.dhall
in  JSON.render (JSON.bool False)
= &quot;false&quot;</code></pre>
<h3 id="type-16">Type</h3>
<pre><code>  ∀(x : Bool)
→ ∀(JSON : Type)
→ ∀ ( json
    : { array : List JSON → JSON
      , bool : Bool → JSON
      , null : JSON
      , number : Double → JSON
      , object : List { mapKey : Text, mapValue : JSON } → JSON
      , string : Text → JSON
      }
    )
→ JSON</code></pre>
<hr>
<h2 id="jsonkeytext">JSON/keyText</h2>
<p>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.</p>
<p>Both key and value are fixed to Text. Take a look at <code>Record/keyValue</code> for a polymorphic version.</p>
<h3 id="type-17">Type</h3>
<pre><code>∀(key : Text) → ∀(value : Text) → { mapKey : Text, mapValue : Text }</code></pre>
<hr>
<h2 id="jsonkeyvalue">JSON/keyValue</h2>
<p>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.</p>
<h3 id="type-18">Type</h3>
<pre><code>∀(v : Type) → ∀(key : Text) → ∀(value : v) → { mapKey : Text, mapValue : v }</code></pre>
<hr>
<h2 id="jsonnull">JSON/null</h2>
<p>Create a JSON null</p>
<pre><code>let JSON = ./package.dhall
in  JSON.render JSON.null
= &quot;null&quot;</code></pre>
<h3 id="type-19">Type</h3>
<pre><code>  ∀(JSON : Type)
→ ∀ ( json
    : { array : List JSON → JSON
      , bool : Bool → JSON
      , null : JSON
      , number : Double → JSON
      , object : List { mapKey : Text, mapValue : JSON } → JSON
      , string : Text → JSON
      }
    )
→ JSON</code></pre>
<hr>
<h2 id="jsonnumber">JSON/number</h2>
<p>Create a JSON number from a Dhall <code>Double</code></p>
<pre><code>let JSON = ./package.dhall
in  JSON.render (JSON.number 42.0)
= &quot;42.0&quot;

let JSON = ./package.dhall
in  JSON.render (JSON.number -1.5e-10)
= &quot;-1.5e-10&quot;</code></pre>
<h3 id="type-20">Type</h3>
<pre><code>  ∀(x : Double)
→ ∀(JSON : Type)
→ ∀ ( json
    : { array : List JSON → JSON
      , bool : Bool → JSON
      , null : JSON
      , number : Double → JSON
      , object : List { mapKey : Text, mapValue : JSON } → JSON
      , string : Text → JSON
      }
    )
→ JSON</code></pre>
<hr>
<h2 id="jsonobject">JSON/object</h2>
<p>Create a JSON object from a Dhall <code>Map</code></p>
<pre><code>let JSON = ./package.dhall
in  JSON.render
    ( JSON.object
      [ { mapKey = &quot;foo&quot;, mapValue = JSON.number 1.0 }
      , { mapKey = &quot;bar&quot;, mapValue = JSON.bool True  }
      ]
    )
= &quot;{ \&quot;foo\&quot;: 1.0, \&quot;bar\&quot;: true }&quot;

let JSON/Type = ./Type
let JSON = ./package.dhall
in  JSON.render
    (JSON.object ([] : List { mapKey : Text, mapValue : JSON/Type }))
= &quot;{ }&quot;</code></pre>
<h3 id="type-21">Type</h3>
<pre><code>  ∀ ( x
    : List
        { mapKey : Text
        , mapValue :
              ∀(JSON : Type)
            → ∀ ( json
                : { array : List JSON → JSON
                  , bool : Bool → JSON
                  , null : JSON
                  , number : Double → JSON
                  , object : List { mapKey : Text, mapValue : JSON } → JSON
                  , string : Text → JSON
                  }
                )
            → JSON
        }
    )
→ ∀(JSON : Type)
→ ∀ ( json
    : { array : List JSON → JSON
      , bool : Bool → JSON
      , null : JSON
      , number : Double → JSON
      , object : List { mapKey : Text, mapValue : JSON } → JSON
      , string : Text → JSON
      }
    )
→ JSON</code></pre>
<hr>
<h2 id="jsonrender">JSON/render</h2>
<p>Render a <code>JSON</code> value as <code>Text</code></p>
<p>This is useful for debugging <code>JSON</code> values or for tests. For anything more sophisticated you should use <code>dhall-to-json</code> or <code>dhall-to-yaml</code></p>
<pre><code>let JSON = ./package.dhall

in  JSON.render
    ( JSON.array
      [ JSON.bool True
      , JSON.string &quot;Hello&quot;
      , JSON.object
        [ { mapKey = &quot;foo&quot;, mapValue = JSON.null       }
        , { mapKey = &quot;bar&quot;, mapValue = JSON.number 1.0 }
        ]
      ]
    )
= &quot;[ true, \&quot;Hello\&quot;, { \&quot;foo\&quot;: null, \&quot;bar\&quot;: 1.0 } ]&quot;</code></pre>
<h3 id="type-22">Type</h3>
<pre><code>  ∀ ( j
    :   ∀(JSON : Type)
      → ∀ ( json
          : { array : List JSON → JSON
            , bool : Bool → JSON
            , null : JSON
            , number : Double → JSON
            , object : List { mapKey : Text, mapValue : JSON } → JSON
            , string : Text → JSON
            }
          )
      → JSON
    )
→ Text</code></pre>
<hr>
<h2 id="jsonstring">JSON/string</h2>
<p>Create a JSON string from Dhall <code>Text</code></p>
<pre><code>let JSON = ./package.dhall
in  JSON.render (JSON.string &quot;ABC $ \&quot; 🙂&quot;)
= &quot;\&quot;ABC \\u0024 \\\&quot; 🙂\&quot;&quot;

let JSON = ./package.dhall
in  JSON.render (JSON.string &quot;&quot;)
= &quot;\&quot;\&quot;&quot;</code></pre>
<h3 id="type-23">Type</h3>
<pre><code>  ∀(x : Text)
→ ∀(JSON : Type)
→ ∀ ( json
    : { array : List JSON → JSON
      , bool : Bool → JSON
      , null : JSON
      , number : Double → JSON
      , object : List { mapKey : Text, mapValue : JSON } → JSON
      , string : Text → JSON
      }
    )
→ JSON</code></pre>
<hr>
<h2 id="listall">List/all</h2>
<p>Returns <code>True</code> if the supplied function returns <code>True</code> for all elements in the <code>List</code></p>
<h3 id="type-24">Type</h3>
<pre><code>∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → Bool</code></pre>
<hr>
<h2 id="listany">List/any</h2>
<p>Returns <code>True</code> if the supplied function returns <code>True</code> for any element in the <code>List</code></p>
<h3 id="type-25">Type</h3>
<pre><code>∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → Bool</code></pre>
<hr>
<h2 id="listbuild">List/build</h2>
<p><code>build</code> is the inverse of <code>fold</code></p>
<h3 id="type-26">Type</h3>
<pre><code>  ∀(a : Type)
→ (∀(list : Type) → ∀(cons : a → list → list) → ∀(nil : list) → list)
→ List a</code></pre>
<hr>
<h2 id="listconcat">List/concat</h2>
<p>Concatenate a <code>List</code> of <code>List</code>s into a single <code>List</code></p>
<h3 id="type-27">Type</h3>
<pre><code>∀(a : Type) → ∀(xss : List (List a)) → List a</code></pre>
<hr>
<h2 id="listconcatmap">List/concatMap</h2>
<p>Transform a list by applying a function to each element and flattening the results</p>
<h3 id="type-28">Type</h3>
<pre><code>∀(a : Type) → ∀(b : Type) → ∀(f : a → List b) → ∀(xs : List a) → List b</code></pre>
<hr>
<h2 id="listfilter">List/filter</h2>
<p>Only keep elements of the list where the supplied function returns <code>True</code></p>
<p>Examples:</p>
<h3 id="type-29">Type</h3>
<pre><code>∀(a : Type) → ∀(f : a → Bool) → ∀(xs : List a) → List a</code></pre>
<hr>
<h2 id="listfold">List/fold</h2>
<p><code>fold</code> is the primitive function for consuming <code>List</code>s</p>
<p>If you treat the list <code>[ x, y, z ]</code> as <code>cons x (cons y (cons z nil))</code>, then a <code>fold</code> just replaces each <code>cons</code> and <code>nil</code> with something else</p>
<h3 id="type-30">Type</h3>
<pre><code>  ∀(a : Type)
→ List a
→ ∀(list : Type)
→ ∀(cons : a → list → list)
→ ∀(nil : list)
→ list</code></pre>
<hr>
<h2 id="listgenerate">List/generate</h2>
<p>Build a list by calling the supplied function on all <code>Natural</code> numbers from <code>0</code> up to but not including the supplied <code>Natural</code> number</p>
<h3 id="type-31">Type</h3>
<pre><code>∀(n : Natural) → ∀(a : Type) → ∀(f : Natural → a) → List a</code></pre>
<hr>
<h2 id="listhead">List/head</h2>
<p>Retrieve the first element of the list</p>
<h3 id="type-32">Type</h3>
<pre><code>∀(a : Type) → List a → Optional a</code></pre>
<hr>
<h2 id="listindexed">List/indexed</h2>
<p>Tag each element of the list with its index</p>
<h3 id="type-33">Type</h3>
<pre><code>∀(a : Type) → List a → List { index : Natural, value : a }</code></pre>
<hr>
<h2 id="listiterate">List/iterate</h2>
<p>Generate a list of the specified length given a seed value and transition function</p>
<h3 id="type-34">Type</h3>
<pre><code>∀(n : Natural) → ∀(a : Type) → ∀(f : a → a) → ∀(x : a) → List a</code></pre>
<hr>
<h2 id="listlast">List/last</h2>
<p>Retrieve the last element of the list</p>
<h3 id="type-35">Type</h3>
<pre><code>∀(a : Type) → List a → Optional a</code></pre>
<hr>
<h2 id="listlength">List/length</h2>
<p>Returns the number of elements in a list</p>
<h3 id="type-36">Type</h3>
<pre><code>∀(a : Type) → List a → Natural</code></pre>
<hr>
<h2 id="listmap">List/map</h2>
<p>Transform a list by applying a function to each element</p>
<h3 id="type-37">Type</h3>
<pre><code>∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(xs : List a) → List b</code></pre>
<hr>
<h2 id="listnull">List/null</h2>
<p>Returns <code>True</code> if the <code>List</code> is empty and <code>False</code> otherwise</p>
<h3 id="type-38">Type</h3>
<pre><code>∀(a : Type) → ∀(xs : List a) → Bool</code></pre>
<hr>
<h2 id="listreplicate">List/replicate</h2>
<p>Build a list by copying the given element the specified number of times</p>
<h3 id="type-39">Type</h3>
<pre><code>∀(n : Natural) → ∀(a : Type) → ∀(x : a) → List a</code></pre>
<hr>
<h2 id="listreverse">List/reverse</h2>
<p>Reverse a list</p>
<h3 id="type-40">Type</h3>
<pre><code>∀(a : Type) → List a → List a</code></pre>
<hr>
<h2 id="listshifted">List/shifted</h2>
<p>Combine a <code>List</code> of <code>List</code>s, offsetting the <code>index</code> of each element by the number of elements in preceding lists</p>
<h3 id="type-41">Type</h3>
<pre><code>  ∀(a : Type)
→ ∀(kvss : List (List { index : Natural, value : a }))
→ List { index : Natural, value : a }</code></pre>
<hr>
<h2 id="listunzip">List/unzip</h2>
<p>Unzip a <code>List</code> into two separate <code>List</code>s</p>
<h3 id="type-42">Type</h3>
<pre><code>  ∀(a : Type)
→ ∀(b : Type)
→ ∀(xs : List { _1 : a, _2 : b })
→ { _1 : List a, _2 : List b }</code></pre>
<hr>
<h2 id="locationtype">Location/Type</h2>
<p>This is the union type returned when you import something <code>as Location</code></p>
<h3 id="type-43">Type</h3>
<pre><code>Type</code></pre>
<hr>
<h2 id="mapentry">Map/Entry</h2>
<p>The type of each key-value pair in a <code>Map</code></p>
<h3 id="type-44">Type</h3>
<pre><code>∀(k : Type) → ∀(v : Type) → Type</code></pre>
<hr>
<h2 id="maptype">Map/Type</h2>
<p>This is the canonical way to encode a dynamic list of key-value pairs.</p>
<p>Tools (such as <code>dhall-to-json</code>/<code>dhall-to-yaml</code> will recognize values of this type and convert them to maps/dictionaries/hashes in the target language</p>
<p>For example, <code>dhall-to-json</code> converts a Dhall value like this:</p>
<pre><code>[ { mapKey = &quot;foo&quot;, mapValue = 1 }
, { mapKey = &quot;bar&quot;, mapValue = 2 }
] : ./Map Text Natural</code></pre>
<p>… to a JSON value like this:</p>
<pre><code>{ &quot;foo&quot;: 1, &quot;bar&quot;, 2 }</code></pre>
<h3 id="type-45">Type</h3>
<pre><code>∀(k : Type) → ∀(v : Type) → Type</code></pre>
<hr>
<h2 id="mapkeys">Map/keys</h2>
<p>Get all of the keys of a <code>Map</code> as a <code>List</code></p>
<h3 id="type-46">Type</h3>
<pre><code>∀(k : Type) → ∀(v : Type) → ∀(xs : List { mapKey : k, mapValue : v }) → List k</code></pre>
<hr>
<h2 id="mapmap">Map/map</h2>
<p>Transform a <code>Map</code> by applying a function to each value</p>
<h3 id="type-47">Type</h3>
<pre><code>  ∀(k : Type)
→ ∀(a : Type)
→ ∀(b : Type)
→ ∀(f : a → b)
→ ∀(m : List { mapKey : k, mapValue : a })
→ List { mapKey : k, mapValue : b }</code></pre>
<hr>
<h2 id="mapvalues">Map/values</h2>
<p>Get all of the values of a <code>Map</code> as a <code>List</code></p>
<h3 id="type-48">Type</h3>
<pre><code>∀(k : Type) → ∀(v : Type) → ∀(xs : List { mapKey : k, mapValue : v }) → List v</code></pre>
<hr>
<h2 id="monoid">Monoid</h2>
<p>Any function <code>f</code> that is a <code>Monoid</code> must satisfy the following law:</p>
<pre><code>t  : Type
f  : ./Monoid t
xs : List (List t)

f (./List/concat t xs) = f (./map (List t) t f xs)</code></pre>
<p>Examples:</p>
<pre><code>./Bool/and
    : ./Monoid Bool
./Bool/or
    : ./Monoid Bool
./Bool/even
    : ./Monoid Bool
./Bool/odd
    : ./Monoid Bool
./List/concat
    : ∀(a : Type) → ./Monoid (List a)
./List/shifted
    : ∀(a : Type) → ./Monoid (List { index : Natural, value : a })
./Natural/sum
    : ./Monoid Natural
./Natural/product
    : ./Monoid Natural
./Optional/head
    : ∀(a : Type) → ./Monoid (Optional a)
./Optional/last
    : ∀(a : Type) → ./Monoid (Optional a)
./Text/concat
    : ./Monoid Text</code></pre>
<h3 id="type-49">Type</h3>
<pre><code>∀(m : Type) → Type</code></pre>
<hr>
<h2 id="naturalbuild">Natural/build</h2>
<p><code>build</code> is the inverse of <code>fold</code></p>
<h3 id="type-50">Type</h3>
<pre><code>  (   ∀(natural : Type)
    → ∀(succ : natural → natural)
    → ∀(zero : natural)
    → natural
  )
→ Natural</code></pre>
<hr>
<h2 id="naturalenumerate">Natural/enumerate</h2>
<p>Generate a list of numbers from <code>0</code> up to but not including the specified number</p>
<h3 id="type-51">Type</h3>
<pre><code>∀(n : Natural) → List Natural</code></pre>
<hr>
<h2 id="naturalequal">Natural/equal</h2>
<p><code>equal</code> checks if two Naturals are equal.</p>
<h3 id="type-52">Type</h3>
<pre><code>∀(a : Natural) → ∀(b : Natural) → Bool</code></pre>
<hr>
<h2 id="naturaleven">Natural/even</h2>
<p>Returns <code>True</code> if a number if even and returns <code>False</code> otherwise</p>
<h3 id="type-53">Type</h3>
<pre><code>Natural → Bool</code></pre>
<hr>
<h2 id="naturalfold">Natural/fold</h2>
<p><code>fold</code> is the primitive function for consuming <code>Natural</code> numbers</p>
<p>If you treat the number <code>3</code> as <code>succ (succ (succ zero))</code> then a <code>fold</code> just replaces each <code>succ</code> and <code>zero</code> with something else</p>
<h3 id="type-54">Type</h3>
<pre><code>  Natural
→ ∀(natural : Type)
→ ∀(succ : natural → natural)
→ ∀(zero : natural)
→ natural</code></pre>
<hr>
<h2 id="naturalgreaterthan">Natural/greaterThan</h2>
<p><code>greaterThan</code> checks if one Natural is strictly greater than another.</p>
<h3 id="type-55">Type</h3>
<pre><code>∀(x : Natural) → ∀(y : Natural) → Bool</code></pre>
<hr>
<h2 id="naturalgreaterthanequal">Natural/greaterThanEqual</h2>
<p><code>greaterThanEqual</code> checks if one Natural is greater than or equal to another.</p>
<h3 id="type-56">Type</h3>
<pre><code>∀(x : Natural) → ∀(y : Natural) → Bool</code></pre>
<hr>
<h2 id="naturaliszero">Natural/isZero</h2>
<p>Returns <code>True</code> if a number is <code>0</code> and returns <code>False</code> otherwise</p>
<h3 id="type-57">Type</h3>
<pre><code>Natural → Bool</code></pre>
<hr>
<h2 id="naturallessthan">Natural/lessThan</h2>
<p><code>lessThan</code> checks if one Natural is strictly less than another.</p>
<h3 id="type-58">Type</h3>
<pre><code>∀(x : Natural) → ∀(y : Natural) → Bool</code></pre>
<hr>
<h2 id="naturallessthanequal">Natural/lessThanEqual</h2>
<p><code>lessThanEqual</code> checks if one Natural is less than or equal to another.</p>
<h3 id="type-59">Type</h3>
<pre><code>∀(x : Natural) → ∀(y : Natural) → Bool</code></pre>
<hr>
<h2 id="naturalodd">Natural/odd</h2>
<p>Returns <code>True</code> if a number is odd and returns <code>False</code> otherwise</p>
<h3 id="type-60">Type</h3>
<pre><code>Natural → Bool</code></pre>
<hr>
<h2 id="naturalproduct">Natural/product</h2>
<p>Multiply all the numbers in a <code>List</code></p>
<h3 id="type-61">Type</h3>
<pre><code>∀(xs : List Natural) → Natural</code></pre>
<hr>
<h2 id="naturalshow">Natural/show</h2>
<p>Render a <code>Natural</code> number as <code>Text</code> using the same representation as Dhall source code (i.e. a decimal number)</p>
<h3 id="type-62">Type</h3>
<pre><code>Natural → Text</code></pre>
<hr>
<h2 id="naturalsubtract">Natural/subtract</h2>
<p><code>subtract m n</code> computes <code>n - m</code>, truncating to <code>0</code> if <code>m &gt; n</code></p>
<h3 id="type-63">Type</h3>
<pre><code>Natural → Natural → Natural</code></pre>
<hr>
<h2 id="naturalsum">Natural/sum</h2>
<p>Add all the numbers in a <code>List</code></p>
<h3 id="type-64">Type</h3>
<pre><code>∀(xs : List Natural) → Natural</code></pre>
<hr>
<h2 id="naturaltodouble">Natural/toDouble</h2>
<p>Convert a <code>Natural</code> number to the corresponding <code>Double</code></p>
<h3 id="type-65">Type</h3>
<pre><code>∀(n : Natural) → Double</code></pre>
<hr>
<h2 id="naturaltointeger">Natural/toInteger</h2>
<p>Convert a <code>Natural</code> number to the corresponding <code>Integer</code></p>
<h3 id="type-66">Type</h3>
<pre><code>Natural → Integer</code></pre>
<hr>
<h2 id="optionalall">Optional/all</h2>
<p>Returns <code>False</code> if the supplied function returns <code>False</code> for a present element and <code>True</code> otherwise:</p>
<h3 id="type-67">Type</h3>
<pre><code>∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Bool</code></pre>
<hr>
<h2 id="optionalany">Optional/any</h2>
<p>Returns <code>True</code> if the supplied function returns <code>True</code> for a present element and <code>False</code> otherwise</p>
<h3 id="type-68">Type</h3>
<pre><code>∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Bool</code></pre>
<hr>
<h2 id="optionalbuild">Optional/build</h2>
<p><code>build</code> is the inverse of <code>fold</code></p>
<h3 id="type-69">Type</h3>
<pre><code>  ∀(a : Type)
→ (   ∀(optional : Type)
    → ∀(just : a → optional)
    → ∀(nothing : optional)
    → optional
  )
→ Optional a</code></pre>
<hr>
<h2 id="optionalconcat">Optional/concat</h2>
<p>Flatten two <code>Optional</code> layers into a single <code>Optional</code> layer</p>
<h3 id="type-70">Type</h3>
<pre><code>∀(a : Type) → ∀(x : Optional (Optional a)) → Optional a</code></pre>
<hr>
<h2 id="optionalfilter">Optional/filter</h2>
<p>Only keep an <code>Optional</code> element if the supplied function returns <code>True</code></p>
<h3 id="type-71">Type</h3>
<pre><code>∀(a : Type) → ∀(f : a → Bool) → ∀(xs : Optional a) → Optional a</code></pre>
<hr>
<h2 id="optionalfold">Optional/fold</h2>
<p><code>fold</code> is the primitive function for consuming <code>Optional</code> values</p>
<h3 id="type-72">Type</h3>
<pre><code>  ∀(a : Type)
→ Optional a
→ ∀(optional : Type)
→ ∀(just : a → optional)
→ ∀(nothing : optional)
→ optional</code></pre>
<hr>
<h2 id="optionalhead">Optional/head</h2>
<p>Returns the first non-empty <code>Optional</code> value in a <code>List</code></p>
<h3 id="type-73">Type</h3>
<pre><code>∀(a : Type) → ∀(xs : List (Optional a)) → Optional a</code></pre>
<hr>
<h2 id="optionallast">Optional/last</h2>
<p>Returns the last non-empty <code>Optional</code> value in a <code>List</code></p>
<h3 id="type-74">Type</h3>
<pre><code>∀(a : Type) → ∀(xs : List (Optional a)) → Optional a</code></pre>
<hr>
<h2 id="optionallength">Optional/length</h2>
<p>Returns <code>1</code> if the <code>Optional</code> value is present and <code>0</code> if the value is absent</p>
<h3 id="type-75">Type</h3>
<pre><code>∀(a : Type) → ∀(xs : Optional a) → Natural</code></pre>
<hr>
<h2 id="optionalmap">Optional/map</h2>
<p>Transform an <code>Optional</code> value with a function</p>
<h3 id="type-76">Type</h3>
<pre><code>∀(a : Type) → ∀(b : Type) → ∀(f : a → b) → ∀(o : Optional a) → Optional b</code></pre>
<hr>
<h2 id="optionalnull">Optional/null</h2>
<p>Returns <code>True</code> if the <code>Optional</code> value is absent and <code>False</code> if present</p>
<h3 id="type-77">Type</h3>
<pre><code>∀(a : Type) → ∀(xs : Optional a) → Bool</code></pre>
<hr>
<h2 id="optionaltolist">Optional/toList</h2>
<p>Convert an <code>Optional</code> value into the equivalent <code>List</code></p>
<h3 id="type-78">Type</h3>
<pre><code>∀(a : Type) → ∀(o : Optional a) → List a</code></pre>
<hr>
<h2 id="optionalunzip">Optional/unzip</h2>
<p>Unzip an <code>Optional</code> value into two separate <code>Optional</code> values</p>
<h3 id="type-79">Type</h3>
<pre><code>  ∀(a : Type)
→ ∀(b : Type)
→ ∀(xs : Optional { _1 : a, _2 : b })
→ { _1 : Optional a, _2 : Optional b }</code></pre>
<hr>
<h2 id="textconcat">Text/concat</h2>
<p>Concatenate all the <code>Text</code> values in a <code>List</code></p>
<h3 id="type-80">Type</h3>
<pre><code>∀(xs : List Text) → Text</code></pre>
<hr>
<h2 id="textconcatmap">Text/concatMap</h2>
<p>Transform each value in a <code>List</code> into <code>Text</code> and concatenate the result</p>
<h3 id="type-81">Type</h3>
<pre><code>∀(a : Type) → ∀(f : a → Text) → ∀(xs : List a) → Text</code></pre>
<hr>
<h2 id="textconcatmapsep">Text/concatMapSep</h2>
<p>Transform each value in a <code>List</code> to <code>Text</code> and then concatenate them with a separator in between each value</p>
<h3 id="type-82">Type</h3>
<pre><code>  ∀(separator : Text)
→ ∀(a : Type)
→ ∀(f : a → Text)
→ ∀(elements : List a)
→ Text</code></pre>
<hr>
<h2 id="textconcatsep">Text/concatSep</h2>
<p>Concatenate a <code>List</code> of <code>Text</code> values with a separator in between each value</p>
<h3 id="type-83">Type</h3>
<pre><code>∀(separator : Text) → ∀(elements : List Text) → Text</code></pre>
<hr>
<h2 id="textdefault">Text/default</h2>
<p>Unwrap an <code>Optional</code> <code>Text</code> value, defaulting <code>None</code> to <code>""</code></p>
<h3 id="type-84">Type</h3>
<pre><code>∀(o : Optional Text) → Text</code></pre>
<hr>
<h2 id="textdefaultmap">Text/defaultMap</h2>
<p>Transform the value in an <code>Optional</code> into <code>Text</code>, defaulting <code>None</code> to <code>""</code></p>
<h3 id="type-85">Type</h3>
<pre><code>∀(a : Type) → ∀(f : a → Text) → ∀(o : Optional a) → Text</code></pre>
<hr>
<h2 id="textshow">Text/show</h2>
<p>Render a <code>Text</code> literal as its own representation as Dhall source code (i.e. a double-quoted string literal)</p>
<h3 id="type-86">Type</h3>
<pre><code>Text → Text</code></pre>
<hr>
<h2 id="xmltype">XML/Type</h2>
<p>Dhall encoding of an arbitrary XML element</p>
<p>For example, the following XML element:</p>
<pre><code>&lt;foo n=&quot;1&quot;&gt;&lt;bar&gt;baz&lt;/bar&gt;&lt;/foo&gt;</code></pre>
<p>… corresponds to the following Dhall expression:</p>
<pre><code>λ(XML : Type)
 → λ ( xml
     : { text :
           Text → XML
       , element :
             { attributes :
                 List { mapKey : Text, mapValue : Text }
             , content :
                 List XML
             , name :
                 Text
             }
           → XML
       }
     )
 → xml.element
   { attributes =
       [ { mapKey = &quot;n&quot;, mapValue = &quot;1&quot; } ]
   , content =
       [ xml.element
         { attributes =
             [] : List { mapKey : Text, mapValue : Text }
         , content =
             [ xml.text &quot;baz&quot; ]
         , name =
             &quot;bar&quot;
         }
       ]
   , name =
       &quot;foo&quot;
   }</code></pre>
<h3 id="type-87">Type</h3>
<pre><code>Type</code></pre>
<hr>
<h2 id="xmlattribute">XML/attribute</h2>
<p>Builds a key-value record with a Text key and value. -}</p>
<p>let attribute : Text → Text → { mapKey : Text, mapValue : Text } = λ(key : Text) → λ(value : Text) → { mapKey = key, mapValue = value }</p>
<p>in attribute</p>
<h3 id="type-88">Type</h3>
<pre><code>∀(key : Text) → ∀(value : Text) → { mapKey : Text, mapValue : Text }</code></pre>
<hr>
<h2 id="xmlelement">XML/element</h2>
<p>Create an XML element value.</p>
<pre><code>let XML = ./package.dhall

in  XML.render
    ( XML.element
      { name = &quot;foo&quot;
      , attributes = XML.emptyAttributes
      , content =
          [ XML.leaf { name = &quot;bar&quot;, attributes = [ XML.attribute &quot;n&quot; &quot;1&quot; ] }
          , XML.leaf { name = &quot;baz&quot;, attributes = [ XML.attribute &quot;n&quot; &quot;2&quot; ] }
          ]
      }
    )

= &quot;&lt;foo&gt;&lt;bar n=\&quot;1\&quot;/&gt;&lt;baz n=\&quot;2\&quot;/&gt;&lt;/foo&gt;&quot;</code></pre>
<h3 id="type-89">Type</h3>
<pre><code>  ∀ ( elem
    : { attributes : List { mapKey : Text, mapValue : Text }
      , content :
          List
            (   ∀(XML : Type)
              → ∀ ( xml
                  : { element :
                          { attributes : List { mapKey : Text, mapValue : Text }
                          , content : List XML
                          , name : Text
                          }
                        → XML
                    , text : Text → XML
                    }
                  )
              → XML
            )
      , name : Text
      }
    )
→ ∀(XML : Type)
→ ∀ ( xml
    : { element :
            { attributes : List { mapKey : Text, mapValue : Text }
            , content : List XML
            , name : Text
            }
          → XML
      , text : Text → XML
      }
    )
→ XML</code></pre>
<hr>
<h2 id="xmlemptyattributes">XML/emptyAttributes</h2>
<p>Create an empty XML attribute List. -}</p>
<p>[] : List { mapKey : Text, mapValue : Text }</p>
<h3 id="type-90">Type</h3>
<pre><code>List { mapKey : Text, mapValue : Text }</code></pre>
<hr>
<h2 id="xmlleaf">XML/leaf</h2>
<p>Create an XML element value without child elements.</p>
<pre><code>let XML = ./package.dhall

in  XML.render (XML.leaf { name = &quot;foobar&quot;, attributes = XML.emptyAttributes })

= &quot;&lt;foobar/&gt;&quot;</code></pre>
<h3 id="type-91">Type</h3>
<pre><code>  ∀ ( elem
    : { attributes : List { mapKey : Text, mapValue : Text }, name : Text }
    )
→ ∀(XML : Type)
→ ∀ ( xml
    : { element :
            { attributes : List { mapKey : Text, mapValue : Text }
            , content : List XML
            , name : Text
            }
          → XML
      , text : Text → XML
      }
    )
→ XML</code></pre>
<hr>
<h2 id="xmlrender">XML/render</h2>
<p>Render an <code>XML</code> value as <code>Text</code></p>
<p><em>WARNING:</em> rendering does not include any XML injection mitigations, therefore it should not be used to process arbitrary strings into element attributes or element data.</p>
<p>For indentation and schema validation, see the <code>xmllint</code> utility bundled with libxml2.</p>
<pre><code>let XML = ./package.dhall

in  XML.render
    ( XML.node
      { name = &quot;foo&quot;
      , attributes = [ XML.attribute &quot;a&quot; &quot;x&quot;, XML.attribute &quot;b&quot; (Natural/show 2) ]
      , content = [ XML.leaf { name = &quot;bar&quot;, attributes = XML.emptyAttributes } ]
      }
    )
= &quot;&lt;foo a=\&quot;x\&quot; b=\&quot;2\&quot;&gt;&lt;bar/&gt;&lt;/foo&gt;&quot;</code></pre>
<h3 id="type-92">Type</h3>
<pre><code>  ∀ ( x
    :   ∀(XML : Type)
      → ∀ ( xml
          : { element :
                  { attributes : List { mapKey : Text, mapValue : Text }
                  , content : List XML
                  , name : Text
                  }
                → XML
            , text : Text → XML
            }
          )
      → XML
    )
→ Text</code></pre>
<hr>
<h2 id="xmltext">XML/text</h2>
<p>Create a Text value to be inserted into an XML element as content.</p>
<pre><code>let XML = ./package.dhall

in  XML.render
    ( XML.node
      { name = &quot;location&quot;
      , attributes = XML.emptyAttributes
      , content = [ XML.text &quot;/foo/bar&quot; ]
      }
    )
= &quot;&lt;location&gt;/foo/bar&lt;/location&gt;&quot;</code></pre>
<h3 id="type-93">Type</h3>
<pre><code>  ∀(d : Text)
→ ∀(XML : Type)
→ ∀ ( xml
    : { element :
            { attributes : List { mapKey : Text, mapValue : Text }
            , content : List XML
            , name : Text
            }
          → XML
      , text : Text → XML
      }
    )
→ XML</code></pre>
<hr>
</body>
</html>
	#!/usr/bin/env nix-shell
	#!nix-shell -i bash -p bash -p lr -p pandoc

	set -euo pipefail

	preludeDir="${1:?dir please}"

	# each file (except package.dhall) starts with a multiline-comment with markdown docstrings.
	# {- maybe docstring
	# docstring
	# maybe docstring -}
	parseDocstringForFile () {
	local doc=$(sed -n \
	-e '/^{-/,/-}$/ p' \
	"$1" \
	\| sed -e '1s/^{-\s*//' \
	\| sed -e '$s/\s*-}$//')
	if [ "$doc" = "" ]; then
	printf 'WARNING: %s has no docstring\n' "$1" >&2
	fi
	printf '%s' "$doc"
	}


	tmp=$(mktemp -d)

	for file in $(lr -t "type = f" -s "$preludeDir" "$preludeDir"); do
	# those are the export files
	if [ "$(basename "$file")" = "package.dhall" ]; then
	continue
	fi
	# printf '%s\n' "$tmp/$file"
	echo "## $file"
	echo
	parseDocstringForFile "$preludeDir/$file"
	echo
	# TODO: build helper dhall executable that can print
	# the type of expressions while caching all imports.
	# (use dhall-flycheck code for that)
	echo
	echo "### Type"
	echo '```'
	(
	# don’t use the cache to preserve variable names
	export XDG_CACHE_HOME=/var/empty
	printf '(./%spackage.dhall).%s\n' "$preludeDir" "${file/\//.}" \
	\| dhall resolve \
	\| dhall type
	)
	echo '```'
	echo
	echo "<hr>"
	done \| pandoc --standalone --to=html5