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

[Dominik Schrempf]

Chiming in here, maybe I missed something. Liquid Haskell is great, but in this
case, in my opinion, easier is better:

newtype LeftFoo = LeftFoo !Int

newtype RightFoo = RightFoo !Char

data Foo = LFoo LeftFoo | RFoo RightFoo – Probably with strictness annotations.

isLeftFoo :: Foo -> Bool
isLeftFoo (LFoo _) = True
isLeftFoo _ = False

takesOnlyLeftFoo :: LeftFoo -> Int
takesOnlyLeftFoo (LeftFoo i) = i

Dominik

Patrick L Redmond via Haskell-Cafe <haskell-cafe at haskell.org> writes:

>  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.
>
> _______________________________________________
> 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.