const package:dhall

Constants for a pure type system The axioms are:

⊦ Type : Kind
⊦ Kind : Sort

... and the valid rule pairs are:

⊦ Type ↝ Type : Type  -- Functions from terms to terms (ordinary functions)
⊦ Kind ↝ Type : Type  -- Functions from types to terms (type-polymorphic functions)
⊦ Sort ↝ Type : Type  -- Functions from kinds to terms
⊦ Kind ↝ Kind : Kind  -- Functions from types to types (type-level functions)
⊦ Sort ↝ Kind : Sort  -- Functions from kinds to types (kind-polymorphic functions)
⊦ Sort ↝ Sort : Sort  -- Functions from kinds to kinds (kind-level functions)

Note that Dhall does not support functions from terms to types and therefore Dhall is not a dependently typed language

Const c                                  ~  c

Parse a single constructor of a union.

Function used to transform Haskell constructor names into their corresponding Dhall alternative names

How to map a Dhall union field name to a Haskell constructor. Note: The constructorName of SingleConstructor will be passed to this function, too.

Name of the constructor

Constructor t post-composes the constructorModifier from options with the value-level version of t, obtained with TextFunction

ShowConstructor x                        ~  showConstructor x

SetSingletonConstructors t replaces the singletonConstructors from options with the value-level version of t.

Convert a type of kind SingletonConstructors into a value of type SingletonConstructors

addConstructorModifier f options post-composes the constructorModifier from options with f.

setSingletonConstructors v options replaces the singletonConstructors from options with v.

This type specifies how to model a Haskell constructor with 1 field in Dhall For example, consider the following Haskell datatype definition:

data Example = Foo { x :: Double } | Bar Double

Depending on which option you pick, the corresponding Dhall type could be:

< Foo : Double | Bar : Double >                   -- Bare

< Foo : { x : Double } | Bar : { _1 : Double } >  -- Wrapped

< Foo : { x : Double } | Bar : Double >           -- Smart

Specify how to handle constructors with only one field. The default is Smart

Specify how to encode an alternative by using the default ToDhall instance for that type.

Specify how to encode an alternative by providing an explicit Encoder for that alternative.

Parse the showConstructor keyword This corresponds to the showConstructor rule from the official grammar

Generate a Haskell type with more than one constructor from a Dhall union type.

Generate a Haskell type with one constructor from any Dhall type. To generate a constructor with multiple named fields, supply a Dhall record type. This does not support more than one anonymous field.