Data kinds in Haskell to implement an n-way Either

gistfile1.txt

ghci> data OneOf :: [*] -> * where Zero :: a -> OneOf (a ': xs); Succ :: OneOf xs -> OneOf (a ': xs)
ghci> let foo = Zero 'a'
ghci> let bar = Succ (Zero 42)
ghci> let baz = Succ (Succ (Zero True))
ghci> :t [foo, bar, baz]
[foo, bar, baz]
  :: [OneOf ((':) * Char ((':) * Integer ((':) * Bool xs)))]
  

Anyone wanting to try this, you'll need:

{-# LANGUAGE GADTs  #-}
{-# LANGUAGE KindSignatures  #-}
{-# LANGUAGE TypeOperators  #-}
{-# LANGUAGE DataKinds  #-}

@runarorama It seems pattern matching on that would be quite verbose if one were to use it as an extended Either.

@travisrudd: Yeah, a hundred-way coproduct would be pretty terrible to deconstruct.

@travisrudd: You could probably use the new pattern synonyms to make it nicer if you actually were going to use something like this.