Some research that I'm doing right now (err… will be doing when I've caught up from a long weekend's-worth of emails) includes a type-level case, just like you're describing. I've been thinking more at a theoretical level to date, and it makes me want to cry thinking about the ambiguity of the arrows… but good point, nonetheless. The type-level case isn't much a topic of the research, as it's easily implementable in terms of closed type families, but it reduces the difference in syntax between terms and types, which is more central to the work. Richard On Dec 2, 2013, at 1:13 AM, Mike Ledger wrote:
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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe