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/