Mike Ledger | 2 Dec 07:13 2013

Type-level case

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
(Continue reading)

Richard Eisenberg | 2 Dec 21:17 2013

Re: Type-level case

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,
(Continue reading)


Gmane