How to use polymorphic type constructors in dhall

Question

I am trying to define a polymorphic type in Dhall. In Haskell it would look like:

data MyType a = Some a | SomethingElse

To do so I have defined this function in Dhall (mkMyType.dhall):

let SomethingElse = ./SomethingElse.dhall  in λ(a : Type) → < some : a | somethingElse : SomethingElse >

I have also defined a function that returns the constructors for that type, given a (./mkMyTypeConstructor.dhall):

λ(a : Type) → constructors (./mkMyType.dhall a)

Now, in order to use it I need to do something like:

(./mkMyTypeConstructor.dhall Text).some "foo"

Is this the right way to do this?

Finally, what would be ideal to have in my use case would be a type that would type check both against for instance a Text such as "foo" and a custom type, for instance { somethingElse: {} }. Is this possible?

Answer 1

I'll use a union type analogous to Haskell's Either to keep the following examples self-contained.

Suppose we save the following Either.dhall file:

-- Either.dhall
λ(a : Type) → λ(b : Type) → < Left : a | Right : b >

We *could provide a makeEither.dhall file like this:

-- makeEither.dhall
λ(a : Type) → λ(b : Type) → constructors (./Either.dhall a b)

... and then we could use that file like this:

[ (./makeEither.dhall Text Natural).Left "Foo"
, (./makeEither.dhall Text Natural).Right 1
]

... but that that would not be ergonomic.

For example, writing ./makeEither.dhall Text Natural repeatedly is not necessary since we can reduce the repetition using a let expression, like this:

    let either = ./makeEither.dhall Text Natural

in  [ either.Left "Foo", either.Right 1 ]

Also, note that we could have used constructors and Either.dhall directly in about the same amount of space:

    let either = constructors (./Either.dhall Text Natural)

in  [ either.Left "Foo", either.Right 1 ]

... which means that we no longer need the intermediate makeEither.dhall file any longer.

The final example is the approach I would recommend. Specifically:

• Use a let expression to avoid repeated use of the constructors keyword
• Have the end user call constructors themselves instead of doing so for them

For your latter question, I think that should go in a separate StackOverflow question.

Edit: Note that the constructors keyword is now obsolete and you can now just write:

let either = ./Either.dhall Text Natural

in  [ either.Left "Foo", either.Right 1 ]

For more details, see:

• Migration: Deprecation of constructors keyword