[Haskell-cafe] selectively allow alternatives in a sum type
Olaf Klinke
olf at aatal-apotheke.de
Wed Aug 31 10:27:25 UTC 2022
> Dear Café,
>
> Is there prior art/existing packages for the following? Is it maybe functional programming folklore? Is it a sign of bad program design?
> Sometimes I feel the need to selectively allow or disallow alternatives
> in a sum type. That is, suppose we have a sum type
>
> data Foo = LeftFoo !A | RightFoo !B
>
> and at some places in the program we want the type system to enforce
> that only the constructor LeftFoo can be used. My solution would be to
> make the type higher rank:
>
> data Foo' f = LeftFoo' !A | RightFoo' !(f B)
> type Foo = Foo' Identity
> type LeftFoo = Foo' (Const' Void) -- can not construct a RightFoo'
>
> The advantage over defining LeftFoo as an entirely different type is
> that Foo and LeftFoo can share functions operating entirely on the left
> option.
>
> Olaf
Henning and Will both suggested accessor type classes. I am fond of my
solution because it uses plain algebraic data types, no classes, GADTs
or type-level lists. David, can you elaborate how this collides with
Coercible? What surprised me is that when writing a function
f :: LeftFoo -> r
GHC did not warn me (-Wincomplete-patterns) about missing cases when f
only uses the LeftFoo' pattern match. Hence the fact that
RightFoo' :: Const Void B -> LeftFoo
is the empty function must somehow be known to the compiler. Nice!
Olaf
More information about the Haskell-Cafe
mailing list