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
