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

Oleg Grenrus oleg.grenrus at iki.fi
Tue Aug 30 14:10:01 UTC 2022


Trees that grow is essentially this, but using type families.

    data Foo ksi
        = LeftFoo !(XLeftFoo ksi) !A
        | RightFoo !(XRightFoo ksi) !B

    type family XLeftFoo ksi :: Type
    type family XRightFoo ksi :: Type

Then you can define

    data Both
    type instance XLeftFoo  Both = ()
    type instance XRightFoo Both = ()

or

    data OnlyLeft
    type instance XLeftFoo  OnlyLeft = ()
    type instance XRightFoo OnlyLeft = Void

---

Third option is to simply have parametrized data:

   data Foo b
       = LeftFoo !A
       | RIghtFoo !b

   type FooBoth = Foo B
   type FooOnlyLeft = Foo Void

---

Sometimes I prefer a higher-kinded data approach, especially if there is
very little variants needed, and they are "uniform" (e.g. second variant
doesn't have some fields).
Yet, sometimes simple parameterized data is simplest approach
(especially as you get stuff for free by deriving Traversable!).

On the other hand, if type is big and have many uniform extension points
(even if there are few different combinations), then HKD becomes
boilerplate heavy as well.
The drawback of TTG, is that writing polymorphic code (i.e. which work
for any or some `ksi`s) is not very fun: a lot of equality constraints etc.

- Oleg

On 30.8.2022 16.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.


More information about the Haskell-Cafe mailing list