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