Re: Q: Types in GADT pattern match

30 Oct 2017

      Right, but I think Gabor's suggestion here is for type checking of the pattern to be done first, and then capturing the coercions
that were brought into scope by the pattern match.

data Foo a where
  Bar :: Foo [a]

foo :: Foo a -> ()
foo Bar = <body> -- we know (a ~ [b]) here, for some b

The pattern match on Bar in foo gives us the equality assumption on the right hand side, but
we don't have an easy way of capturing 'b' - which we might want to do for, say, visible type application inside <body>.

foo' :: Foo a -> ()
foo' (Bar :: Foo a) = <body>

of course works, but it only gives us access to 'a' in <body>.

foo'' :: Foo a -> ()
foo'' (Bar :: Foo [c]) = <body>

This would mean that in addition to (a ~ [b]), for some b, we would get (a ~ [c]), for our new c. This then gives (b ~ c),
essentially giving us access to the existential b. Of course we would need to check that our scoped type signature
doesn't introduce bogus coercions, like

foo''' :: Foo a -> ()
foo''' (Bar :: Foo [[c]]) = <body>

is clearly invalid, because (a ~ [b]) and (a ~ [[c]]) would need (b ~ [c]), which we can't prove from the given assumptions.

Cheers,
Csongor

On 30 Oct 2017, 12:13 +0000, Brandon Allbery , wrote:
...
...
On Mon, Oct 30, 2017 at 5:14 AM, Gabor Greif  wrote:
...
My original question, though, is not answered yet, namely why not to
detect that we are about to pattern match on a GADT constructor and
allow the programmer to capture the *refined* type with her type
annotation. Sure this would necessitate a change to the type checker,
but would also increase the expressive power a bit.
Is there some fundamental problem with this? Or simply nobody wanted
to do this yet? Would it be hard to implement type checking *after*
refinement on GADT(-like) patterns?
I wouldn't be surprised if type checking is precisely what enables refinement, making this a bit chicken-and-egg.
--
brandon s allbery kf8nh                               sine nomine associates
allbery.b@gmail.com                                  ballbery@sinenomine.net
unix, openafs, kerberos, infrastructure, xmonad        http://sinenomine.net
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Q: Types in GADT pattern match

Csongor Kiss