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

[Patrick L Redmond]

>
> Sometimes I feel the need to selectively allow or disallow alternatives
>

This seems like the kind of lightweight property that Liquid Haskell (a GHC
plugin) is especially suited for. Here's a small example of "at some places
in the program we want the type system to enforce that only the constructor
LeftFoo can be used."

data Foo = LeftFoo !Int | RightFoo !Char

{-@ measure isLeftFoo @-}
isLeftFoo :: Foo -> Bool
isLeftFoo LeftFoo{} = True
isLeftFoo _ = False

{-@ takesOnlyLeftFoo :: {x:Foo | isLeftFoo x} -> Int @-}
takesOnlyLeftFoo :: Foo -> Int
takesOnlyLeftFoo (LeftFoo i) = i

I've taken Olaf's hypothetical Foo and swapped in Int for A and Char for B,
defined a function *isLeftFoo* that returns True for LeftFoo-constructed
Foos, and I call *isLeftFoo* in the type of a function that is meant to
only be called with LeftFoo values.

This syntax in the mushroom-at-symbol comments is a refinement type. It has
the same structure as the haskell type `Foo -> Int` but adds a precondition
on the input that *isLeftFoo* returns True. When you compile your project
with Liquid Haskell, the precondition will be checked at compile time by
checking that callers establish the fact on any value they pass into
*takesOnlyLeftFoo*.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20220901/cc809444/attachment.html>