Hi, In this specific case you could use a GADT: data Foo (only_left :: Bool) where LeftFoo :: A -> Foo only_left RightFoo :: B -> Foo 'False onlyLeft :: Foo 'True -> String onlyLeft = \case LeftFoo _a -> "an A" anyFoo :: Foo a -> String anyFoo = \case LeftFoo _a -> "an A" RightFoo _b -> "a B" But it isn't very modular. A more heavyweight alternative is to use some kind of variants instead. See https://docs.haskus.org/variant.html for example where I describe my implementation. I wish we had more compiler support for constructor polymorphism like this though. Sylvain On 30/08/2022 15:30, Olaf Klinke wrote:
Dear Café,
Is there prior art/existing packages for the following? Is it maybefunctional 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 use a strict version of Data.Functor.Const and make the type higher rank:
newtype Const' a b = Const' !a -- Const' Void b ~ Void -- Const' () b ~ ()
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
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.