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 <[email protected]> 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 <[email protected]> On Behalf Of Richard Eisenberg
> Sent: 29 March 2021 03:18
> To: Alexis King <[email protected]>
> Cc: [email protected]
> Subject: Re: Type inference of singular matches on GADTs
>
>
>
>
> On Mar 26, 2021, at 8:41 PM, Alexis King <[email protected]
> <mailto:[email protected]>> 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
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
