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