[Haskell-cafe] Type-level case

[Mike Ledger]

Hi. This is more of a brain dump than anything well thought out, but 
it's been in the back of my mind for a while.

It's occurred to me that with the upcoming release of GHC 7.8, which 
features closed type families, we've effectively been given type-level 
pattern matching that behaves the same as expression-level pattern matching.

What I think could follow is type-level case syntax. For example:

   type family Example a where
     Example 100 = 60
     Example 120 = 15
     Example x   = x * 30
   contrived :: Sing a -> Sing b -> Sing (Example (a+b))

might instead be expressed as:

   contrived :: Sing a -> Sing b -> Sing (case a+b of
     100 -> 60
     120 -> 15
     x   -> x*30) -- but with something other than -> in the patterns,
                  -- since that conflicts with the type (->), and there
                  -- are probably too many arrows already


Similarly I think if-then-else could be lifted to the type level, also.

Some problems with this are that it could pollute "complex" type 
signatures even further (although currently the situation isn't very 
good due to haddock/ghc not listing type family instances), and it would 
get quite cumbersome quickly to have to type out

   contrived2 :: Proxy (a, b)
              -> Sing (case a+b of { 100 -> 60; 120 -> 15; x -> x*30 })
              -> ...


-- Mike