Q: Types in GADT pattern match

Mon Oct 30 20:58:25 UTC 2017

On 10/30/17, Csongor Kiss <kiss.csongor.kiss at gmail.com> 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 <allbery.b at gmail.com>, wrote:
>> > On Mon, Oct 30, 2017 at 5:14 AM, Gabor Greif <ggreif at gmail.com> 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 at gmail.com
>>  ballbery at sinenomine.net
>> unix, openafs, kerberos, infrastructure, xmonad
>>  http://sinenomine.net
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>