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

[Olaf Klinke]

In my real use case, things are not as simple as the example Foo, of
course. 
There are fields of the same type, distributed across the choices, but
some are optional in some choices and mandatory in others. Rank-1
parameters permit a range including, but not limited, to
	Indentity  -- mandatory
	Maybe      -- optional
	Const ()   -- missing
	Const Void -- constructor disallowed

e.g. 

data Bar left right = LeftBar A (left O) | RightBar A B (right O)

type OptionalLeftMandatoryRight = Bar Maybe Identity
-- encodes: "If B is present so must be O, but if not, O is optional".

type OnlyA = Bar (Const ()) (Const Void)
-- isomorphic to A 

getO :: Applicative f => Bar f Identity -> f O
getO (LeftBar _ o) = o
getO (RightBar _ _ (Identity o)) = pure o

getA :: Bar left right -> A
getA (LeftBar a _) = a
getA (RightBar a _ _) = a

With distinct data types for LeftBar and RightBar, the functions getO,
getA in their generality would only be possible via type classes. In
some sense, the type parameters act as an explicit type class
dictionary. I believe this is in the spirit of Trees that Grow, 
where the combination (left,right) = (Maybe,Identity) would be encoded
in a type family. 

Olaf

On Thu, 2022-09-01 at 22:33 +0200, Dominik Schrempf wrote:
> 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.