Search code examples
haskelldhall

How to use polymorphic type constructors in dhall

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?

Solution

  • 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: