[Haskell-cafe] Type union

[Adam Gundry]

Hi Arnaud,

You can't quite write what you asked for, but you can get pretty close,
as long as you don't mind Peano naturals rather than integer literals,
and an extra (partially-defined) element:

{-# LANGUAGE GADTs, TypeOperators #-}

type (:|) = Either
infixr 5 :|

data In x xs where
  Zero :: In x (x :| xs)
  Suc  :: In x xs -> In x (y :| xs)

inj :: In x xs -> x -> xs
inj Zero    = Left
inj (Suc n) = Right . inj n

data Void

f :: Int -> Int :| String :| Bool :| Void
f 0 = inj Zero             1
f 1 = inj (Suc Zero)       "foo"
f 2 = inj (Suc (Suc Zero)) True

I'm not sure how useful this is in practice, however.

Hope this helps,

Adam


On 15/09/14 14:14, Arnaud Bailly wrote:
> Hello,
> I have a somewhat similar problem, trying to achieve union types but for
> the purpose of defining the set of allowable outcomes of a function. I
> have tried naively to define a type operator a :| b and I would like to
> be able to define a function like :
> 
> f :: Int -> Int :| String :| Bool
> f 1 = in 1 1
> f 2 = in 2 "foo"
> f 3 = in 3 True
> 
> e.g. the codomain type is indexed by integers. I think this should be
> possible, even without full dependent typing given that I only expect to
> use literals
> 
> My type-level-fu is really lacking so help would be appreciated.
> 
> Regards,
> 
> --
> Arnaud Bailly
> FoldLabs Associate: http://foldlabs.com

-- 
Adam Gundry, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com/