Sum Type Subsets

#1

I’m learning Dhall at the moment by porting my Alacritty configuration to Dhall. The configuration allows for slightly different values depending on the platform. For example, there’s a key startup_mode which allows let StartupMode = < Windowed | Maximized | Fullscreen > on Linux, but let StartupMode = < Windowed | Maximized | Fullscreen | SimpleFullscreen > on MacOS.

Is it possible to enforce this through Dhall? Basically, I’d imagine that the entire configuration can exist as MacOS and as a Linux variant. I don’t even know how I’d do this in Haskell to be honest. I have some vague notions of data Config a = MacOS a | Linux a. Ideally I’d like to make it impossible to construct a Linux configuration with MacOS values somewhere.

1 Like
#2

You could potentially do something like

let UniversalStartupMode = <Windowed | Maximized | Fullscreen >

let MacOSStartupMode = <UniversalMode : UniversalStartupMode | SimpleFullscreen >

let LinuxStartupMode = UniversalStartupMode

There is very possibly a better approach though.

#3

There’s a longstanding missing feature to add something like //\\, but for combining union types, instead. In other words, you could imagine a dual \\// (⩔) operator that behaves like this:

let UniversalStartupMode = < Windowed | Maximized | Fullscreen >

let MacOSStartupMode = UniversalStartupMode \\// < SimpleFullScreen >

let LinuxStartupmode = UniversalStartupMode

For more details, see: https://github.com/dhall-lang/dhall-lang/issues/175

How exactly you use those two types depends on the context, but here is a guess at what I think you might have meant:

let Config
      : { startup_mode : Type } → Type
      = λ(args : { startup_mode : Type }) → { startup_mode : args.startup_mode }

let MacOSConfig : Type = Config { startup_mode = MacOSStartupMode }

let LinuxConfig : Type = Config { startup_mode = LinuxStartupmode }

let example : MacOSConfig = { startup_mode = MacOSStartupMode.Maximized }
2 Likes
#4

Thank you very much for the detailed response. I’ll watch the linked github issue for activity then!

1 Like