<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">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.<div class=""><br class=""></div><div class="">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 ->).</div><div class=""><br class=""></div><div class="">EX1: \x @-> case x of HNil -> blah</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">EX2: \x @-> (x, case x of HNit -> blah)</div><div class=""><br class=""></div><div class="">Same as EX1.</div><div class=""><br class=""></div><div class="">EX3: \x @-> case x of { HNil1 -> blah; HNil2 -> blah }</div><div class=""><br class=""></div><div class="">Same as EX1. There is still a unique type for which the patten-match is exhaustive.</div><div class=""><br class=""></div><div class="">EX4: Reject. There are multiple valid types, and we don't know which one to pick. This is like classic untouchable-variables territory.</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">EX6: Reject. No type leads to exhaustive matches.</div><div class=""><br class=""></div><div class="">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.</div><div class=""><br class=""></div><div class="">Richard</div><div class=""><br class=""></div><div class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Mar 29, 2021, at 5:00 AM, Simon Peyton Jones <<a href="mailto:simonpj@microsoft.com" class="">simonpj@microsoft.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="WordSection1" style="page: WordSection1; caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;"><div style="margin: 0cm 0cm 0cm 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class="">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.<o:p class=""></o:p></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class="">As I wrote in another post on this thread, it’s a bit tricky. <o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class="">What would you expect of (EX1)<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-family: "Courier New";" class=""> \x -> case x of HNil -> blah<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class="">Here the lambda and the case are separated<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class="">Now (EX2)<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-family: "Courier New";" class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm 0cm 0cm 18pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-family: "Courier New";" class="">\x -> (x, case x of HNil -> blah)<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class="">Here the lambda and the case are separated more, and x is used twice.<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class="">What if there are more data constructors that share a common return type? (EX3)<o:p class=""></o:p></span></div><div style="margin: 0cm 0cm 0cm 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-family: "Courier New";" class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm 0cm 0cm 18pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-family: "Courier New";" class="">data HL2 a where<o:p class=""></o:p></span></div><div style="margin: 0cm 0cm 0cm 36pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class=""><span style="font-family: "Courier New";" class="">HNil1 :: HL2 []<o:p class=""></o:p></span></div><div style="margin: 0cm 0cm 0cm 36pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class=""><span style="font-family: "Courier New";" class="">HNil2 :: HL2 []<o:p class=""></o:p></span></div><div style="margin: 0cm 0cm 0cm 36pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class=""><span style="font-family: "Courier New";" class="">HCons :: …blah…<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-family: "Courier New";" class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm 0cm 0cm 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-family: "Courier New";" class="">\x -> case x of { HNil1 -> blah; HNil 2 -> blah }<o:p class=""></o:p></span></div><div style="margin: 0cm 0cm 0cm 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-family: "Courier New";" class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class="">Here HNil1 and HNil2 both return HL2 []. Is that “singular”? <o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class="">What if one was a bit more general than the other? Do we seek the least common generalisation of the alternatives given? (EX4)<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm 0cm 0cm 18pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-family: "Courier New";" class="">data HL3 a where<o:p class=""></o:p></span></div><div style="margin: 0cm 0cm 0cm 36pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class=""><span style="font-family: "Courier New";" class="">HNil1 :: HL2 [Int]<o:p class=""></o:p></span></div><div style="margin: 0cm 0cm 0cm 36pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class=""><span style="font-family: "Courier New";" class="">HNil2 :: HL2 [a]<o:p class=""></o:p></span></div><div style="margin: 0cm 0cm 0cm 36pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class=""><span style="font-family: "Courier New";" class="">HCons :: …blah…<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-family: "Courier New";" class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm 0cm 0cm 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-family: "Courier New";" class="">\x -> case x of { HNil1 -> blah; HNil 2 -> blah }<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class="">What if the cases were incompatible? (EX5)<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm 0cm 0cm 18pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-family: "Courier New";" class="">data HL4 a where<o:p class=""></o:p></span></div><div style="margin: 0cm 0cm 0cm 36pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class=""><span style="font-family: "Courier New";" class="">HNil1 :: HL2 [Int]<o:p class=""></o:p></span></div><div style="margin: 0cm 0cm 0cm 36pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class=""><span style="font-family: "Courier New";" class="">HNil2 :: HL2 [Bool]<o:p class=""></o:p></span></div><div style="margin: 0cm 0cm 0cm 36pt; font-size: 11pt; font-family: Calibri, sans-serif; text-indent: 36pt;" class=""><span style="font-family: "Courier New";" class="">HCons :: …blah…<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-family: "Courier New";" class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm 0cm 0cm 36pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-family: "Courier New";" class="">\x -> case x of { HNil1 -> blah; HNil 2 -> blah }<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class="">Would you expect that to somehow generalise to `HL4 [a] -> blah`?<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><br class="">What if x matched multiple times, perhaps on different constructors (EX6)<br class=""><br class=""><o:p class=""></o:p></span></div><div style="margin: 0cm 0cm 0cm 18pt; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-family: "Courier New";" class="">\x -> (case s of HNil1 -> blah1; case x of HNil2 -> blah)<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class="">The water gets deep quickly here. I don’t (yet) see an obviously-satisfying design point that isn’t massively ad-hoc.<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class="">Simon<o:p class=""></o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span class=""><o:p class=""> </o:p></span></div><div style="border-style: none none none solid; border-left-width: 1.5pt; border-left-color: blue; padding: 0cm 0cm 0cm 4pt;" class=""><div class=""><div style="border-style: solid none none; border-top-width: 1pt; border-top-color: rgb(225, 225, 225); padding: 3pt 0cm 0cm;" class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><b class=""><span lang="EN-US" class="">From:</span></b><span lang="EN-US" class=""><span class="Apple-converted-space"> </span>ghc-devs <<a href="mailto:ghc-devs-bounces@haskell.org" class="">ghc-devs-bounces@haskell.org</a>><span class="Apple-converted-space"> </span><b class="">On Behalf Of<span class="Apple-converted-space"> </span></b>Richard Eisenberg<br class=""><b class="">Sent:</b><span class="Apple-converted-space"> </span>29 March 2021 03:18<br class=""><b class="">To:</b><span class="Apple-converted-space"> </span>Alexis King <<a href="mailto:lexi.lambda@gmail.com" class="">lexi.lambda@gmail.com</a>><br class=""><b class="">Cc:</b><span class="Apple-converted-space"> </span><a href="mailto:ghc-devs@haskell.org" class="">ghc-devs@haskell.org</a><br class=""><b class="">Subject:</b><span class="Apple-converted-space"> </span>Re: Type inference of singular matches on GADTs<o:p class=""></o:p></span></div></div></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><br class=""><br class=""><o:p class=""></o:p></div><blockquote style="margin-top: 5pt; margin-bottom: 5pt;" class=""><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class="">On Mar 26, 2021, at 8:41 PM, Alexis King <<a href="mailto:lexi.lambda@gmail.com" style="color: blue; text-decoration: underline;" class="">lexi.lambda@gmail.com</a>> wrote:<o:p class=""></o:p></div></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><span style="font-size: 9pt; font-family: Helvetica, sans-serif;" class="">If there’s a single principal type that makes my function well-typed<span class="apple-converted-space"> </span><i class="">and exhaustive</i>, I’d really like GHC to pick it.</span><o:p class=""></o:p></div></div></blockquote></div><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class="">I think this is the key part of Alexis's plea: that the type checker take into account exhaustivity in choosing how to proceed.<o:p class=""></o:p></div></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class="">Another way to think about this:<o:p class=""></o:p></div></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div></div><blockquote style="margin-top: 5pt; margin-bottom: 5pt;" class=""><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class="">f1 :: HList '[] -> ()<o:p class=""></o:p></div></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class="">f1 HNil = ()<o:p class=""></o:p></div></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class="">f2 :: HList as -> ()<o:p class=""></o:p></div></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class="">f2 HNil = ()<o:p class=""></o:p></div></div></blockquote><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class="">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.<o:p class=""></o:p></div></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class="">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.<o:p class=""></o:p></div></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class="">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.<o:p class=""></o:p></div></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class="">But first: does this match your understanding?<o:p class=""></o:p></div></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class=""><o:p class=""> </o:p></div></div><div class=""><div style="margin: 0cm; font-size: 11pt; font-family: Calibri, sans-serif;" class="">Richard</div></div></div></div></div></blockquote></div><br class=""></div></body></html>