Questions and possible improvements for Dhall.TH

[ndwarshuis]

This might be several issues, but I thought I would leave them together (for now) since they might have overlapping solutions and affect the same small set of functions.

For my specific use-case, I have dhall types that I would like to serve as the source of truth, and I would like to generate haskell types from these using Dhall.TH.

This approach appears to have several limitations. Some of these might already have existing solutions/workarounds that I missed, but if not they are potential features/enhancements.

1. Importing higher-kinded type constructors

I would like to create the following Haskell type:

data Foo a = Foo { bar :: a }

from the following Dhall code using makeHaskellTypes:

\(t : Type) -> { bar : a }

Unfortunately this doesn't appear to be supported per the two DataD clauses in toDeclaration which simply have blank lists for the type variable fields.

I'm assuming it is possible to inspect the Dhall syntax and figure out if there are arguments that need to be added to the type constructor, but I'm also not sure if there are theoretical/technical limitations for why this isn't implemented.

2. Support for strictness annotations

Going with the above example again, I don't see a way to add bangs to fields:

data Foo a = Foo { bar :: !a }

This also appears to be a hardcoded limitation in toConstructor which sets strictness (and unpack) to "no".

The simple way I can think of for implementing this would be to extend GenerateOptions (or make a new type like it) which will include a list of fields to which bangs should be applied. I imagine adding UNPACK to this would also be useful.

3. Coercing Haskell-specific types from more general Dhall Types

Suppose I have the following Dhall type:

{ silly : List (List (List Natural)) }

and I want to import it as the following Haskell type:

data Foo = Foo { silly :: [Vector (Seq Natural)] }

The key ideas are a) mapping a Dhall List to a specific 'list-like' type in Haskell (or any analogous type pair) and b) doing so at any level within the type as necessary.

I'm not sure of the best way to implement such a feature, but I imagine the cleanest way would be something like type annotations at the template Haskell level (if that exists, which I'm not sure). Something like:

-- not real haskell code...
Dhall.TH.makeHaskellTypes
    [ (SingleConstructor "Foo" "Foo" "./Foo.dhall" :: Foo { silly :: [Vector (Seq Natural)] })
    ]

Like (2) above, this would also be easier on a per-field basis since not all fields would need to be coerced, but again I have no idea what "valid" notation might look like.

[Gabriella439]

(1) is a little tricky, but probably possible to do. I probably wouldn't have time to do it myself but I'd accept a PR to support that

The hardest part about (2) and (3) is the desired API. I feel like at that point it's more ergonomic to define the desired Haskell type directly instead of generating the type using TemplateHaskell. As a concrete example, if you're writing something like :: Foo { silly :: [Vector (Seq Natural)] } then you've already written out the desired Haskell type so you don't need to generate it using TemplateHaskell

[ndwarshuis]

@Gabriella439

(1) is a little tricky, but probably possible to do. I probably wouldn't have time to do it myself but I'd accept a PR to support that

Ok, I can take a shot at a PR.

The hardest part about (2) and (3) is the desired API. I feel like at that point it's more ergonomic to define the desired Haskell type directly instead of generating the type using TemplateHaskell.

This is a good point.

However, for 2 I think I overcomplicated my original use case by proposing field-level granularity. I'm not sure how many people follow this convention, but I add bangs to all of my fields unless required otherwise (per discussion in this article about 60% down).

Since this is a choice of "lazy by default" or "strict by default" at the type level, the revised API extension I would propose would add a boolean field to GenerateOptions (called useStrictFields or similar), which if set to True would add bangs to all fields. False would be the default to keep with current behavior. This way people who want "strict by default" can get it without having to retype everything (at the cost of overriding one field in GenerateOptions). In the probably rare case where such users want laziness/strictness for only a few fields, then I think it's fair to simply duplicate the Dhall type with the desired strictness annotations.

Would this be an acceptable modification? If so I can also work on a PR for it.

[Gabriella439]

RE: (2), I'd accept a PR adding a field to GenerateOptions to globally customize the behavior to ad bangs to fields

[ndwarshuis]

@Gabriella439 thank you :) I'll work on these

[mmhat]

Closing this as it has been fixed in #2504 .