[Haskell-cafe] selectively allow alternatives in a sum type

[Sylvain Henry]

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.