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 <simo...@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-boun...@haskell.org> On Behalf Of Richard Eisenberg > Sent: 29 March 2021 03:18 > To: Alexis King <lexi.lam...@gmail.com> > Cc: ghc-devs@haskell.org > Subject: Re: Type inference of singular matches on GADTs > > > > > On Mar 26, 2021, at 8:41 PM, Alexis King <lexi.lam...@gmail.com > <mailto:lexi.lam...@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
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs