Open DestyNova opened 4 years ago
I also tried removing the type signature for insert
, and expected the following definition of insertSort'
to be invalid:
insert :: (Ord a) => a -> IncList a -> IncList a
insert y Emp = y :< Emp
insert y (x :< xs)
| y <= x = y :< x :< xs
| otherwise = x :< insert y xs
insertSort' :: (Ord a) => [a] -> IncList a
insertSort' = foldr f b
where
f = insert
b = Emp
However, it typechecked with no problems. Why is this legal, but hoisting the definition of insert
into the insertSort'
function's where
block is rejected (unless a type signature is added to f
)?
Apologies for the basic questions, I'm just keen to understand this. :grinning:
This is in fact a very tricky business I’ll explain once I put my kid to bed but try these two variants
Make the signatures ALL monomorphic Ie replace a with Int
Hoist your local “f” to the top level and don’t write a signature (alternately just erase the dig for insert.)
You’ll find 1 fails but 2 passes. Will explain in a bit!
On Sun, Apr 12, 2020 at 6:56 PM Oisín notifications@github.com wrote:
I also tried removing the type signature for insert, and expected the following definition of insertSort' to be invalid:
insert :: (Ord a) => a -> IncList a -> IncList a
insert y Emp = y :< Emp
insert y (x :< xs)
| y <= x = y :< x :< xs
| otherwise = x :< insert y xs
insertSort' :: (Ord a) => [a] -> IncList a
insertSort' = foldr f b
where
f = insert b = Emp
However, it typechecked with no problems. Why is this legal, but hoisting the definition of insert into the insertSort' function's where block is rejected?
Apologies for the basic questions, I'm just keen to understand this. 😀
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/91#issuecomment-612714266, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAMS4OEVM6JZE7PUAMYKIC3RMJWN5ANCNFSM4MGUXTRQ .
Hi, this has come up MANY times so I decided to write a little blog about it, will post it soon, but here's the draft!
On Sun, Apr 12, 2020 at 7:48 PM Ranjit Jhala jhala@cs.ucsd.edu wrote:
This is in fact a very tricky business I’ll explain once I put my kid to bed but try these two variants
Make the signatures ALL monomorphic Ie replace a with Int
Hoist your local “f” to the top level and don’t write a signature (alternately just erase the dig for insert.)
You’ll find 1 fails but 2 passes. Will explain in a bit!
On Sun, Apr 12, 2020 at 6:56 PM Oisín notifications@github.com wrote:
I also tried removing the type signature for insert, and expected the following definition of insertSort' to be invalid:
insert :: (Ord a) => a -> IncList a -> IncList a
insert y Emp = y :< Emp
insert y (x :< xs)
| y <= x = y :< x :< xs
| otherwise = x :< insert y xs
insertSort' :: (Ord a) => [a] -> IncList a
insertSort' = foldr f b
where
f = insert b = Emp
However, it typechecked with no problems. Why is this legal, but hoisting the definition of insert into the insertSort' function's where block is rejected?
Apologies for the basic questions, I'm just keen to understand this. 😀
— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/91#issuecomment-612714266, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAMS4OEVM6JZE7PUAMYKIC3RMJWN5ANCNFSM4MGUXTRQ .
Thanks for sharing that draft @ranjitjhala, it helped to understand some of the cleverness that was going on (namely, that the use of polymorphic types allows LH to conclude that insert
cannot return an (Ord a) => IncList a
with larger or smaller values than those passed to it in its arguments.... but that a concrete type like IncList Int
would not permit such a guarantee).
However I'm still a bit confused about a couple of points:
f
is omitted, then GHC must infer one. Surely it can't replace the a
with Int
because the error still appears when I remove the test code that calls insertSort'
with a list of integers. So what does it infer? (I tried unsuccessfully to find out in GHCi.)insert
(in "top-level" file scope) is removed, the error doesn't appear:
-- insert :: (Ord a) => a -> IncList a -> IncList a -- GHC still infers this
insert y Emp = y :< Emp
insert y (x :< xs)
| y <= x = y :< x :< xs
| otherwise = x :< insert y xs
insertSort' :: (Ord a) => [a] -> IncList a insertSort' = foldr f b where f = insert b = Emp
I have to admit not being familiar with GHC's concept of existential quantification. Could it be that, at the top-level, a function without a type signature is assumed to be valid "forall" inputs, but moving the definition into the `where` clause of `insertSort'` causes it to be inferred as potentially a partial function, which then causes LH to not treat it as polymorphic?
I've tested that GHC infers the equivalent type signature for `insert` when one hasn't been defined. But I can't quite figure out how to test what it thinks `f`'s signature would be when defined inside `insertSort'`.
Regarding suggestions to make it easier to understand the output of LH, could LH perhaps give a specific hint when it can't prove that some constraints hold in similar situations?
For example, maybe an Elm-style error message like:
(Line xx, col yy) In the function call: f y xs, I couldn't prove that the return value satisfies this constraint: {VV: a | y <= VV}. The (inferred/actual) type signature of f looks like this: (...monomorphic inferred signature...) but I expected to see: (...signature that would allow the proof to continue...) Hint: It may help to give f an explicit polymorphic type signature.
@ranjitjhala Am I correct in understanding that the problem here is the lack of polymorphic recursion in local bindings?
I know that while GHC can infer polymorphic types, it will restrict itself to monomorphic recursion. But I take it that Liquid Haskell can force instantiation of the GHC-inferred types in recursive calls for its own refinement purposes, getting polymorphic recursion this way.
What's not clear to me is why GHC doesn't generalize local local bindings. I thought let generalization was only disabled when certain GHC options were enabled (like GADTs).
Hi @LPTK -- yes that's exactly it. For non-top-level bindings GHC doesn't "generalize" the inferred type, perhaps because (I'm guessing) there is no need to really. For top-level binders you want to generalize otherwise the function is basically useless...
My hunch is that this paper probably articulates the rationale for why local binders are not generalized:
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tldi10-vytiniotis.pdf
In chapter 5, there's a trivially solvable exercise to specify the
insertSort'
function usingfoldr
.The intended solution is presumably that
f = insert
andb = Emp
.But if I "inline" the
insert
function without a type signature, it doesn't work:Again, adding a type signature for
f
helps:Could you explain why it's necessary to add this type signature?