[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