Type inference of singular matches on GADTs

[Simon Peyton Jones]

I'm not saying this is a good idea for GHC or that it's implementable. But the idea of having type inference account for exhaustivity in this way does not seem, a priori, unspecified.

No, but I’m pointing out that specifying it might be tricky, involving some highly non-local reasoning.  I can’t yet see how to write a formal specification.   Note “yet”  -- growth mindset!

Simon

From: Richard Eisenberg <rae at richarde.dev>
Sent: 30 March 2021 04:58
To: Simon Peyton Jones <simonpj at microsoft.com>
Cc: Alexis King <lexi.lambda at gmail.com>; ghc-devs at haskell.org
Subject: Re: Type inference of singular matches on GADTs

As usual, I want to separate out the specification of a feature from the implementation. So let's just focus on specification for now -- with the caveat that there might be no possible implementation of these ideas.

The key innovation I see lurking here is the idea of an *exhaustive* function, where we know that any pattern-match on an argument is always exhaustive. I will write such a thing with @->, in both the type and in the arrow that appears after the lambda. The @-> type is a subtype of -> (and perhaps does not need to be written differently from ->).

EX1: \x @-> case x of HNil -> blah

This is easy: we can infer HList '[] @-> blah's type, because the pattern match is declared to be exhaustive, and no other type grants that property.

EX2: \x @-> (x, case x of HNit -> blah)

Same as EX1.

EX3: \x @-> case x of { HNil1 -> blah; HNil2 -> blah }

Same as EX1. There is still a unique type for which the patten-match is exhaustive.

EX4: Reject. There are multiple valid types, and we don't know which one to pick. This is like classic untouchable-variables territory.

EX5: This is hard. A declarative spec would probably choose HL2 [a] -> ... as you suggest, but there may be no implementation of such an idea.

EX6: Reject. No type leads to exhaustive matches.

I'm not saying this is a good idea for GHC or that it's implementable. But the idea of having type inference account for exhaustivity in this way does not seem, a priori, unspecified.

Richard




On Mar 29, 2021, at 5:00 AM, Simon Peyton Jones <simonpj at microsoft.com<mailto:simonpj at microsoft.com>> wrote:

I haven't thought about how to implement such a thing. At the least, it would probably require some annotation saying that we expect `\HNil -> ()` to be exhaustive (as GHC won't, in general, make that assumption). Even with that, could we get type inference to behave? Possibly.

As I wrote in another post on this thread, it’s a bit tricky.

What would you expect of (EX1)

   \x -> case x of HNil -> blah

Here the lambda and the case are separated

Now (EX2)

\x -> (x, case x of HNil -> blah)

Here the lambda and the case are separated more, and x is used twice.
What if there are more data constructors that share a common return type? (EX3)

data HL2 a where
HNil1 :: HL2 []
HNil2 :: HL2 []
HCons :: …blah…

\x -> case x of { HNil1 -> blah; HNil 2 -> blah  }

Here HNil1 and HNil2 both return HL2 [].   Is that “singular”?

What if one was a bit more general than the other?   Do we seek the least common generalisation of the alternatives given? (EX4)

data HL3 a where
HNil1 :: HL2 [Int]
HNil2 :: HL2 [a]
HCons :: …blah…

\x -> case x of { HNil1 -> blah; HNil 2 -> blah  }

What if the cases were incompatible?  (EX5)

data HL4 a where
HNil1 :: HL2 [Int]
HNil2 :: HL2 [Bool]
HCons :: …blah…

\x -> case x of { HNil1 -> blah; HNil 2 -> blah  }

Would you expect that to somehow generalise to `HL4 [a] -> blah`?

What if x matched multiple times, perhaps on different constructors (EX6)


\x -> (case s of HNil1 -> blah1;  case x of HNil2 -> blah)


The water gets deep quickly here.  I don’t (yet) see an obviously-satisfying design point that isn’t massively ad-hoc.

Simon


From: ghc-devs <ghc-devs-bounces at haskell.org<mailto:ghc-devs-bounces at haskell.org>> On Behalf Of Richard Eisenberg
Sent: 29 March 2021 03:18
To: Alexis King <lexi.lambda at gmail.com<mailto:lexi.lambda at gmail.com>>
Cc: ghc-devs at haskell.org<mailto:ghc-devs at haskell.org>
Subject: Re: Type inference of singular matches on GADTs





On Mar 26, 2021, at 8:41 PM, Alexis King <lexi.lambda at gmail.com<mailto:lexi.lambda at gmail.com>> wrote:

If there’s a single principal type that makes my function well-typed and exhaustive, I’d really like GHC to pick it.

I think this is the key part of Alexis's plea: that the type checker take into account exhaustivity in choosing how to proceed.

Another way to think about this:

f1 :: HList '[] -> ()
f1 HNil = ()

f2 :: HList as -> ()
f2 HNil = ()

Both f1 and f2 are well typed definitions. In any usage site where both are well-typed, they will behave the same. Yet f1 is exhaustive while f2 is not. This isn't really about an open-world assumption or the possibility of extra cases -- it has to do with what the runtime behaviors of the two functions are. f1 never fails, while f2 must check a constructor tag and perhaps throw an exception.

If we just see \HNil -> (), Alexis seems to be suggesting we prefer the f1 interpretation over the f2 interpretation. Why? Because f1 is exhaustive, and when we can choose an exhaustive interpretation, that's probably a good idea to pursue.

I haven't thought about how to implement such a thing. At the least, it would probably require some annotation saying that we expect `\HNil -> ()` to be exhaustive (as GHC won't, in general, make that assumption). Even with that, could we get type inference to behave? Possibly.

But first: does this match your understanding?

Richard

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210330/46b14e12/attachment-0001.html>