What would you expect of
1. \x -> case x of HNil -> blah
Here the lambda and the case are separated.
1. \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?
1. 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?
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 Alexis King
Sent: 20 March 2021 09:41
To: [email protected]
Subject: Type inference of singular matches on GADTs
Hi all,
Today I was writing some code that uses a GADT to represent heterogeneous lists:
data HList as where
HNil :: HList '[]
HCons :: a -> HList as -> HList (a ': as)
This type is used to provide a generic way to manipulate n-ary functions.
Naturally, I have some functions that accept these n-ary functions as
arguments, which have types like this:
foo :: Blah as => (HList as -> Widget) -> Whatsit
The idea is that Blah does some type-level induction on as and supplies the
function with some appropriate values. Correspondingly, my use sites look
something like this:
bar = foo (\HNil -> ...)
Much to my dismay, I quickly discovered that GHC finds these expressions quite
unfashionable, and it invariably insults them:
• Ambiguous type variable ‘as0’ arising from a use of ‘foo’
prevents the constraint ‘(Blah as0)’ from being solved.
The miscommunication is simple enough. I expected that when given an expression
like
\HNil -> ...
GHC would see a single pattern of type HList '[] and consequently infer a type
like
HList '[] -> ...
Alas, it was not to be. It seems GHC is reluctant to commit to the choice of
'[] for as, lest perhaps I add another case to my function in the future.
Indeed, if I were to do that, the choice of '[] would be premature, as as ~ '[]
would only be available within one branch. However, I do not in fact have any
such intention, which makes me quietly wish GHC would get over its anxiety and
learn to be a bit more of a risk-taker.
I ended up taking a look at the OutsideIn(X) paper, hoping to find some
commentary on this situation, but in spite of the nice examples toward the
start about the trickiness of GADTs, I found no discussion of this specific
scenario: a function with exactly one branch and an utterly unambiguous
pattern. Most examples come at the problem from precisely the opposite
direction, trying to tease out a principle type from a collection of branches.
The case of a function (or perhaps more accurately, a case expression) with
only a single branch does not seem to be given any special attention.
Of course, fewer special cases is always nice. I have great sympathy for
generality. Still, I can’t help but feel a little unsatisfied here.
Theoretically, there is no reason GHC cannot treat
\(a `HCons` b `HCons` c `HCons` HNil) -> ...
and
\a b c -> ...
almost identically, with a well-defined principle type and pleasant type
inference properties, but there is no way for me to communicate this to the
typechecker! So, my questions:
1. Have people considered this problem before? Is it discussed anywhere
already?
2. Is my desire here reasonable, or is there some deep philosophical
argument for why my program should be rejected?
3. If it is reasonable, are there any obvious situations where a change
targeted at what I’m describing (vague as that is) would affect programs
negatively, not positively?
I realize this gets rather at the heart of the typechecker, so I don’t intend
to imply a change of this sort should be made frivolously. Indeed, I’m not even
particularly attached to the idea that a change must be made! But I do want to
understand the tradeoffs better, so any insight would be much appreciated.
Thanks,
Alexis
_______________________________________________
ghc-devs mailing list
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
