Re: Q: Types in GADT pattern match

30 Oct 2017

      On 10/30/17, Csongor Kiss  wrote:
...
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>.
Yep. Visible type application on the RHS is what I am after. It is
just user-unfriendly that one has to doubly pattern match on the same
object in order to bring the GADT constructor's type equality into
play.

Thanks Csongor for the expanded reasoning!

    Gabor
...
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