Why does GHC infer a monomorphic type here, even with MonomorphismRestriction disabled? The Next CEO of Stack OverflowResolving the type of `f = f (<*>) pure`NoMonomorphismRestriction helps preserve sharing?How can eta-reduction of a well typed function result in a type error?Can I write such polymorphic function? What language extensions do I need?GHC rewrite rule specialising a function for a type classType Inference in PatternsHow to type check recursive definitions using Algorithm W?What is the monomorphism restriction?Why are higher rank types so fragile in HaskellWhy can't GHC typecheck this function involving polymorphism and existential types?Problems With Type Inference on (^)
Does it take more energy to get to Venus or to Mars?
declare as function pointer and initialize in the same line
Is HostGator storing my password in plaintext?
Return of the Riley Riddles in Reverse
India just shot down a satellite from the ground. At what altitude range is the resulting debris field?
suction cup thing with 1/4 TRS cable?
Was a professor correct to chastise me for writing "Prof. X" rather than "Professor X"?
If the heap is initialized for security, then why is the stack uninitialized?
How easy is it to start Magic from scratch?
ls Ordering[Ordering[list]] optimal?
Fastest way to shutdown Ubuntu Mate 18.10
What makes a siege story/plot interesting?
How can I open an app using Terminal?
Why here is plural "We went to the movies last night."
MAZDA 3 2006 (UK) - poor acceleration then takes off at 3250 revs
Why is there a PLL in CPU?
Does the Brexit deal have to be agreed by both Houses?
WOW air has ceased operation, can I get my tickets refunded?
How to make a variable always equal to the result of some calculations?
Trouble understanding the speech of overseas colleagues
How long to clear the 'suck zone' of a turbofan after start is initiated?
I believe this to be a fraud
Is there a good way to store credentials outside of a password manager?
The King's new dress
Why does GHC infer a monomorphic type here, even with MonomorphismRestriction disabled?
The Next CEO of Stack OverflowResolving the type of `f = f (<*>) pure`NoMonomorphismRestriction helps preserve sharing?How can eta-reduction of a well typed function result in a type error?Can I write such polymorphic function? What language extensions do I need?GHC rewrite rule specialising a function for a type classType Inference in PatternsHow to type check recursive definitions using Algorithm W?What is the monomorphism restriction?Why are higher rank types so fragile in HaskellWhy can't GHC typecheck this function involving polymorphism and existential types?Problems With Type Inference on (^)
This was prompted by Resolving the type of `f = f (<*>) pure`, which discusses a more complicated example, but this one works too.
The following definition compiles without problem:
w :: Integral a => a
w = fromInteger w
...Of course it doesn't work runtime-wise, but that's beside the question. The point is that the definition of w
itself uses a specialised version of w :: Integer
. Clearly that is a suitable instantiation, and therefore typechecks.
However, if we remove the signature, then GHC infers not the above type, but only the concrete one:
w' = fromInteger w'
GHCi> :t w
w :: Integral a => a
GHCi> :t w'
w' :: Integer
Well, when I saw this, I was fairly sure this was the monomorphism restriction at work. It's well known that also e.g.
i = 3
GHCi> :t i
i :: Integer
although i :: Num p => p
would be perfectly possible. And indeed, i :: Num p => p
is inferred if -XNoMonomorphismRestriction
is active, i.e. if the monomorphism restriction is disabled.
However, in case of w'
only the type Integer
is inferred even when the monomorphism restriction is disabled.
To count out that this has something to do with defaulting:
fromFloat :: RealFrac a => Float -> a
q :: RealFrac a => a
q = fromFloat q
q' = fromFloat q'
GHCi> :t q
q :: RealFrac a => a
GHCi> :t q'
q' :: Float
Why is the polymorphic type not inferred?
haskell recursion type-inference parametric-polymorphism
add a comment |
This was prompted by Resolving the type of `f = f (<*>) pure`, which discusses a more complicated example, but this one works too.
The following definition compiles without problem:
w :: Integral a => a
w = fromInteger w
...Of course it doesn't work runtime-wise, but that's beside the question. The point is that the definition of w
itself uses a specialised version of w :: Integer
. Clearly that is a suitable instantiation, and therefore typechecks.
However, if we remove the signature, then GHC infers not the above type, but only the concrete one:
w' = fromInteger w'
GHCi> :t w
w :: Integral a => a
GHCi> :t w'
w' :: Integer
Well, when I saw this, I was fairly sure this was the monomorphism restriction at work. It's well known that also e.g.
i = 3
GHCi> :t i
i :: Integer
although i :: Num p => p
would be perfectly possible. And indeed, i :: Num p => p
is inferred if -XNoMonomorphismRestriction
is active, i.e. if the monomorphism restriction is disabled.
However, in case of w'
only the type Integer
is inferred even when the monomorphism restriction is disabled.
To count out that this has something to do with defaulting:
fromFloat :: RealFrac a => Float -> a
q :: RealFrac a => a
q = fromFloat q
q' = fromFloat q'
GHCi> :t q
q :: RealFrac a => a
GHCi> :t q'
q' :: Float
Why is the polymorphic type not inferred?
haskell recursion type-inference parametric-polymorphism
Doesn't the monomorphism restriction apply only to simple bindings anyways (andw' = fromInteger w'
, being recursive, is not simple)?
– Alec
4 hours ago
@Alec possible, but still – why does something like the monomorphism restriction seem to kick in here?
– leftaroundabout
4 hours ago
I'm probably being dense and missing something here, butfromInteger
has type(Num a) => Integer -> a
, and sincew'
is used as the input tofromInteger
, doesn't that meanInteger
is the only possible type for it? Indeed I'm rather surprised that the version with the polymorphic type signature compiles. (So as I said, probably missing something.)
– Robin Zigmond
4 hours ago
@RobinZigmondInteger
is certainly the only possible monomorphic type forw'
, but asw
demonstrates a polymorphic type is perfectly fine as well. After all, a polymorphic type can be instantiated to a monomorphic one, provided it fulfills the constraints.
– leftaroundabout
4 hours ago
add a comment |
This was prompted by Resolving the type of `f = f (<*>) pure`, which discusses a more complicated example, but this one works too.
The following definition compiles without problem:
w :: Integral a => a
w = fromInteger w
...Of course it doesn't work runtime-wise, but that's beside the question. The point is that the definition of w
itself uses a specialised version of w :: Integer
. Clearly that is a suitable instantiation, and therefore typechecks.
However, if we remove the signature, then GHC infers not the above type, but only the concrete one:
w' = fromInteger w'
GHCi> :t w
w :: Integral a => a
GHCi> :t w'
w' :: Integer
Well, when I saw this, I was fairly sure this was the monomorphism restriction at work. It's well known that also e.g.
i = 3
GHCi> :t i
i :: Integer
although i :: Num p => p
would be perfectly possible. And indeed, i :: Num p => p
is inferred if -XNoMonomorphismRestriction
is active, i.e. if the monomorphism restriction is disabled.
However, in case of w'
only the type Integer
is inferred even when the monomorphism restriction is disabled.
To count out that this has something to do with defaulting:
fromFloat :: RealFrac a => Float -> a
q :: RealFrac a => a
q = fromFloat q
q' = fromFloat q'
GHCi> :t q
q :: RealFrac a => a
GHCi> :t q'
q' :: Float
Why is the polymorphic type not inferred?
haskell recursion type-inference parametric-polymorphism
This was prompted by Resolving the type of `f = f (<*>) pure`, which discusses a more complicated example, but this one works too.
The following definition compiles without problem:
w :: Integral a => a
w = fromInteger w
...Of course it doesn't work runtime-wise, but that's beside the question. The point is that the definition of w
itself uses a specialised version of w :: Integer
. Clearly that is a suitable instantiation, and therefore typechecks.
However, if we remove the signature, then GHC infers not the above type, but only the concrete one:
w' = fromInteger w'
GHCi> :t w
w :: Integral a => a
GHCi> :t w'
w' :: Integer
Well, when I saw this, I was fairly sure this was the monomorphism restriction at work. It's well known that also e.g.
i = 3
GHCi> :t i
i :: Integer
although i :: Num p => p
would be perfectly possible. And indeed, i :: Num p => p
is inferred if -XNoMonomorphismRestriction
is active, i.e. if the monomorphism restriction is disabled.
However, in case of w'
only the type Integer
is inferred even when the monomorphism restriction is disabled.
To count out that this has something to do with defaulting:
fromFloat :: RealFrac a => Float -> a
q :: RealFrac a => a
q = fromFloat q
q' = fromFloat q'
GHCi> :t q
q :: RealFrac a => a
GHCi> :t q'
q' :: Float
Why is the polymorphic type not inferred?
haskell recursion type-inference parametric-polymorphism
haskell recursion type-inference parametric-polymorphism
edited 2 hours ago
leftaroundabout
asked 4 hours ago
leftaroundaboutleftaroundabout
80.1k3119237
80.1k3119237
Doesn't the monomorphism restriction apply only to simple bindings anyways (andw' = fromInteger w'
, being recursive, is not simple)?
– Alec
4 hours ago
@Alec possible, but still – why does something like the monomorphism restriction seem to kick in here?
– leftaroundabout
4 hours ago
I'm probably being dense and missing something here, butfromInteger
has type(Num a) => Integer -> a
, and sincew'
is used as the input tofromInteger
, doesn't that meanInteger
is the only possible type for it? Indeed I'm rather surprised that the version with the polymorphic type signature compiles. (So as I said, probably missing something.)
– Robin Zigmond
4 hours ago
@RobinZigmondInteger
is certainly the only possible monomorphic type forw'
, but asw
demonstrates a polymorphic type is perfectly fine as well. After all, a polymorphic type can be instantiated to a monomorphic one, provided it fulfills the constraints.
– leftaroundabout
4 hours ago
add a comment |
Doesn't the monomorphism restriction apply only to simple bindings anyways (andw' = fromInteger w'
, being recursive, is not simple)?
– Alec
4 hours ago
@Alec possible, but still – why does something like the monomorphism restriction seem to kick in here?
– leftaroundabout
4 hours ago
I'm probably being dense and missing something here, butfromInteger
has type(Num a) => Integer -> a
, and sincew'
is used as the input tofromInteger
, doesn't that meanInteger
is the only possible type for it? Indeed I'm rather surprised that the version with the polymorphic type signature compiles. (So as I said, probably missing something.)
– Robin Zigmond
4 hours ago
@RobinZigmondInteger
is certainly the only possible monomorphic type forw'
, but asw
demonstrates a polymorphic type is perfectly fine as well. After all, a polymorphic type can be instantiated to a monomorphic one, provided it fulfills the constraints.
– leftaroundabout
4 hours ago
Doesn't the monomorphism restriction apply only to simple bindings anyways (and
w' = fromInteger w'
, being recursive, is not simple)?– Alec
4 hours ago
Doesn't the monomorphism restriction apply only to simple bindings anyways (and
w' = fromInteger w'
, being recursive, is not simple)?– Alec
4 hours ago
@Alec possible, but still – why does something like the monomorphism restriction seem to kick in here?
– leftaroundabout
4 hours ago
@Alec possible, but still – why does something like the monomorphism restriction seem to kick in here?
– leftaroundabout
4 hours ago
I'm probably being dense and missing something here, but
fromInteger
has type (Num a) => Integer -> a
, and since w'
is used as the input to fromInteger
, doesn't that mean Integer
is the only possible type for it? Indeed I'm rather surprised that the version with the polymorphic type signature compiles. (So as I said, probably missing something.)– Robin Zigmond
4 hours ago
I'm probably being dense and missing something here, but
fromInteger
has type (Num a) => Integer -> a
, and since w'
is used as the input to fromInteger
, doesn't that mean Integer
is the only possible type for it? Indeed I'm rather surprised that the version with the polymorphic type signature compiles. (So as I said, probably missing something.)– Robin Zigmond
4 hours ago
@RobinZigmond
Integer
is certainly the only possible monomorphic type for w'
, but as w
demonstrates a polymorphic type is perfectly fine as well. After all, a polymorphic type can be instantiated to a monomorphic one, provided it fulfills the constraints.– leftaroundabout
4 hours ago
@RobinZigmond
Integer
is certainly the only possible monomorphic type for w'
, but as w
demonstrates a polymorphic type is perfectly fine as well. After all, a polymorphic type can be instantiated to a monomorphic one, provided it fulfills the constraints.– leftaroundabout
4 hours ago
add a comment |
1 Answer
1
active
oldest
votes
Polymorphic recursion (where a function calls itself at a different type than the one at which it was called) always requires a type signature. The full explanation is in Section 4.4.1 of the Haskell 2010 Report:
If a variable
f
is defined without providing a corresponding type signature declaration, then each use off
outside its own declaration group (see Section 4.5) is treated as having the corresponding inferred, or principal type. However, to ensure that type inference is still possible, the defining occurrence, and all uses off
within its declaration group must have the same monomorphic type (from which the principal type is obtained by generalization, as described in Section 4.5.2).
The same section later presents an example of polymorphic recursion supported by a type signature.
My understanding is that unaided type inference is generally undecidable in the presence of polymorphic recursion, so Haskell doesn't even try.
In this case, the type checker starts with
w :: a
where a
is a meta-variable. Since fromInteger
is called with w
as an argument within its own declaration (and therefore within its declaration group), the type checker unifies a
with Integer
. There are no variables left to generalize.
1
My bachelor was about a simple type inferencer for a subset of Haskell including typeclasses & polymorphic recursion. A very simple approach is to limit the depth of the polymorphic recursion up tok
depth. Most useful cases of polymorphic recursion can be inferred with a very low depth bound (like k=1 or k=2). Anyway Haskell type inference is already undecidable so that's not the only reason why it's not allowed. An other reason is probably performance, it surely makes type inference O(k·f(n)) instead of O(f(n)) since you may need to do all over again for k times.
– Bakuriu
3 hours ago
1
@Bakuriu, I am pretty sure that Haskell 2010 without polymorphic recursion has full type inference--it's basically Hindley-Milner at that point, plus type classes and defaulting. Do you have a reference saying otherwise? As for some limited recursion depth: that sounds like a potentially useful extension, but it has a very different flavor from what the Haskell Report tends to do. I would find such a feature most useful for discovering the right type signatures for polymorphic recursive code.
– dfeuer
2 hours ago
Yes, but I think all extensions to the type systems on top of Haskell2010 make type inference undecidable. Note that for example Type families are "artificially" limited to avoid undecidable instances by forbidding certain well-formed programs by default, so allowing a "k-recursive" polymorphic recursion would not be very different from that case, IMHO.
– Bakuriu
1 hour ago
add a comment |
Your Answer
StackExchange.ifUsing("editor", function ()
StackExchange.using("externalEditor", function ()
StackExchange.using("snippets", function ()
StackExchange.snippets.init();
);
);
, "code-snippets");
StackExchange.ready(function()
var channelOptions =
tags: "".split(" "),
id: "1"
;
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function()
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled)
StackExchange.using("snippets", function()
createEditor();
);
else
createEditor();
);
function createEditor()
StackExchange.prepareEditor(
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader:
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
,
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
);
);
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f55402733%2fwhy-does-ghc-infer-a-monomorphic-type-here-even-with-monomorphismrestriction-di%23new-answer', 'question_page');
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
Polymorphic recursion (where a function calls itself at a different type than the one at which it was called) always requires a type signature. The full explanation is in Section 4.4.1 of the Haskell 2010 Report:
If a variable
f
is defined without providing a corresponding type signature declaration, then each use off
outside its own declaration group (see Section 4.5) is treated as having the corresponding inferred, or principal type. However, to ensure that type inference is still possible, the defining occurrence, and all uses off
within its declaration group must have the same monomorphic type (from which the principal type is obtained by generalization, as described in Section 4.5.2).
The same section later presents an example of polymorphic recursion supported by a type signature.
My understanding is that unaided type inference is generally undecidable in the presence of polymorphic recursion, so Haskell doesn't even try.
In this case, the type checker starts with
w :: a
where a
is a meta-variable. Since fromInteger
is called with w
as an argument within its own declaration (and therefore within its declaration group), the type checker unifies a
with Integer
. There are no variables left to generalize.
1
My bachelor was about a simple type inferencer for a subset of Haskell including typeclasses & polymorphic recursion. A very simple approach is to limit the depth of the polymorphic recursion up tok
depth. Most useful cases of polymorphic recursion can be inferred with a very low depth bound (like k=1 or k=2). Anyway Haskell type inference is already undecidable so that's not the only reason why it's not allowed. An other reason is probably performance, it surely makes type inference O(k·f(n)) instead of O(f(n)) since you may need to do all over again for k times.
– Bakuriu
3 hours ago
1
@Bakuriu, I am pretty sure that Haskell 2010 without polymorphic recursion has full type inference--it's basically Hindley-Milner at that point, plus type classes and defaulting. Do you have a reference saying otherwise? As for some limited recursion depth: that sounds like a potentially useful extension, but it has a very different flavor from what the Haskell Report tends to do. I would find such a feature most useful for discovering the right type signatures for polymorphic recursive code.
– dfeuer
2 hours ago
Yes, but I think all extensions to the type systems on top of Haskell2010 make type inference undecidable. Note that for example Type families are "artificially" limited to avoid undecidable instances by forbidding certain well-formed programs by default, so allowing a "k-recursive" polymorphic recursion would not be very different from that case, IMHO.
– Bakuriu
1 hour ago
add a comment |
Polymorphic recursion (where a function calls itself at a different type than the one at which it was called) always requires a type signature. The full explanation is in Section 4.4.1 of the Haskell 2010 Report:
If a variable
f
is defined without providing a corresponding type signature declaration, then each use off
outside its own declaration group (see Section 4.5) is treated as having the corresponding inferred, or principal type. However, to ensure that type inference is still possible, the defining occurrence, and all uses off
within its declaration group must have the same monomorphic type (from which the principal type is obtained by generalization, as described in Section 4.5.2).
The same section later presents an example of polymorphic recursion supported by a type signature.
My understanding is that unaided type inference is generally undecidable in the presence of polymorphic recursion, so Haskell doesn't even try.
In this case, the type checker starts with
w :: a
where a
is a meta-variable. Since fromInteger
is called with w
as an argument within its own declaration (and therefore within its declaration group), the type checker unifies a
with Integer
. There are no variables left to generalize.
1
My bachelor was about a simple type inferencer for a subset of Haskell including typeclasses & polymorphic recursion. A very simple approach is to limit the depth of the polymorphic recursion up tok
depth. Most useful cases of polymorphic recursion can be inferred with a very low depth bound (like k=1 or k=2). Anyway Haskell type inference is already undecidable so that's not the only reason why it's not allowed. An other reason is probably performance, it surely makes type inference O(k·f(n)) instead of O(f(n)) since you may need to do all over again for k times.
– Bakuriu
3 hours ago
1
@Bakuriu, I am pretty sure that Haskell 2010 without polymorphic recursion has full type inference--it's basically Hindley-Milner at that point, plus type classes and defaulting. Do you have a reference saying otherwise? As for some limited recursion depth: that sounds like a potentially useful extension, but it has a very different flavor from what the Haskell Report tends to do. I would find such a feature most useful for discovering the right type signatures for polymorphic recursive code.
– dfeuer
2 hours ago
Yes, but I think all extensions to the type systems on top of Haskell2010 make type inference undecidable. Note that for example Type families are "artificially" limited to avoid undecidable instances by forbidding certain well-formed programs by default, so allowing a "k-recursive" polymorphic recursion would not be very different from that case, IMHO.
– Bakuriu
1 hour ago
add a comment |
Polymorphic recursion (where a function calls itself at a different type than the one at which it was called) always requires a type signature. The full explanation is in Section 4.4.1 of the Haskell 2010 Report:
If a variable
f
is defined without providing a corresponding type signature declaration, then each use off
outside its own declaration group (see Section 4.5) is treated as having the corresponding inferred, or principal type. However, to ensure that type inference is still possible, the defining occurrence, and all uses off
within its declaration group must have the same monomorphic type (from which the principal type is obtained by generalization, as described in Section 4.5.2).
The same section later presents an example of polymorphic recursion supported by a type signature.
My understanding is that unaided type inference is generally undecidable in the presence of polymorphic recursion, so Haskell doesn't even try.
In this case, the type checker starts with
w :: a
where a
is a meta-variable. Since fromInteger
is called with w
as an argument within its own declaration (and therefore within its declaration group), the type checker unifies a
with Integer
. There are no variables left to generalize.
Polymorphic recursion (where a function calls itself at a different type than the one at which it was called) always requires a type signature. The full explanation is in Section 4.4.1 of the Haskell 2010 Report:
If a variable
f
is defined without providing a corresponding type signature declaration, then each use off
outside its own declaration group (see Section 4.5) is treated as having the corresponding inferred, or principal type. However, to ensure that type inference is still possible, the defining occurrence, and all uses off
within its declaration group must have the same monomorphic type (from which the principal type is obtained by generalization, as described in Section 4.5.2).
The same section later presents an example of polymorphic recursion supported by a type signature.
My understanding is that unaided type inference is generally undecidable in the presence of polymorphic recursion, so Haskell doesn't even try.
In this case, the type checker starts with
w :: a
where a
is a meta-variable. Since fromInteger
is called with w
as an argument within its own declaration (and therefore within its declaration group), the type checker unifies a
with Integer
. There are no variables left to generalize.
edited 2 hours ago
answered 4 hours ago
dfeuerdfeuer
33.5k349133
33.5k349133
1
My bachelor was about a simple type inferencer for a subset of Haskell including typeclasses & polymorphic recursion. A very simple approach is to limit the depth of the polymorphic recursion up tok
depth. Most useful cases of polymorphic recursion can be inferred with a very low depth bound (like k=1 or k=2). Anyway Haskell type inference is already undecidable so that's not the only reason why it's not allowed. An other reason is probably performance, it surely makes type inference O(k·f(n)) instead of O(f(n)) since you may need to do all over again for k times.
– Bakuriu
3 hours ago
1
@Bakuriu, I am pretty sure that Haskell 2010 without polymorphic recursion has full type inference--it's basically Hindley-Milner at that point, plus type classes and defaulting. Do you have a reference saying otherwise? As for some limited recursion depth: that sounds like a potentially useful extension, but it has a very different flavor from what the Haskell Report tends to do. I would find such a feature most useful for discovering the right type signatures for polymorphic recursive code.
– dfeuer
2 hours ago
Yes, but I think all extensions to the type systems on top of Haskell2010 make type inference undecidable. Note that for example Type families are "artificially" limited to avoid undecidable instances by forbidding certain well-formed programs by default, so allowing a "k-recursive" polymorphic recursion would not be very different from that case, IMHO.
– Bakuriu
1 hour ago
add a comment |
1
My bachelor was about a simple type inferencer for a subset of Haskell including typeclasses & polymorphic recursion. A very simple approach is to limit the depth of the polymorphic recursion up tok
depth. Most useful cases of polymorphic recursion can be inferred with a very low depth bound (like k=1 or k=2). Anyway Haskell type inference is already undecidable so that's not the only reason why it's not allowed. An other reason is probably performance, it surely makes type inference O(k·f(n)) instead of O(f(n)) since you may need to do all over again for k times.
– Bakuriu
3 hours ago
1
@Bakuriu, I am pretty sure that Haskell 2010 without polymorphic recursion has full type inference--it's basically Hindley-Milner at that point, plus type classes and defaulting. Do you have a reference saying otherwise? As for some limited recursion depth: that sounds like a potentially useful extension, but it has a very different flavor from what the Haskell Report tends to do. I would find such a feature most useful for discovering the right type signatures for polymorphic recursive code.
– dfeuer
2 hours ago
Yes, but I think all extensions to the type systems on top of Haskell2010 make type inference undecidable. Note that for example Type families are "artificially" limited to avoid undecidable instances by forbidding certain well-formed programs by default, so allowing a "k-recursive" polymorphic recursion would not be very different from that case, IMHO.
– Bakuriu
1 hour ago
1
1
My bachelor was about a simple type inferencer for a subset of Haskell including typeclasses & polymorphic recursion. A very simple approach is to limit the depth of the polymorphic recursion up to
k
depth. Most useful cases of polymorphic recursion can be inferred with a very low depth bound (like k=1 or k=2). Anyway Haskell type inference is already undecidable so that's not the only reason why it's not allowed. An other reason is probably performance, it surely makes type inference O(k·f(n)) instead of O(f(n)) since you may need to do all over again for k times.– Bakuriu
3 hours ago
My bachelor was about a simple type inferencer for a subset of Haskell including typeclasses & polymorphic recursion. A very simple approach is to limit the depth of the polymorphic recursion up to
k
depth. Most useful cases of polymorphic recursion can be inferred with a very low depth bound (like k=1 or k=2). Anyway Haskell type inference is already undecidable so that's not the only reason why it's not allowed. An other reason is probably performance, it surely makes type inference O(k·f(n)) instead of O(f(n)) since you may need to do all over again for k times.– Bakuriu
3 hours ago
1
1
@Bakuriu, I am pretty sure that Haskell 2010 without polymorphic recursion has full type inference--it's basically Hindley-Milner at that point, plus type classes and defaulting. Do you have a reference saying otherwise? As for some limited recursion depth: that sounds like a potentially useful extension, but it has a very different flavor from what the Haskell Report tends to do. I would find such a feature most useful for discovering the right type signatures for polymorphic recursive code.
– dfeuer
2 hours ago
@Bakuriu, I am pretty sure that Haskell 2010 without polymorphic recursion has full type inference--it's basically Hindley-Milner at that point, plus type classes and defaulting. Do you have a reference saying otherwise? As for some limited recursion depth: that sounds like a potentially useful extension, but it has a very different flavor from what the Haskell Report tends to do. I would find such a feature most useful for discovering the right type signatures for polymorphic recursive code.
– dfeuer
2 hours ago
Yes, but I think all extensions to the type systems on top of Haskell2010 make type inference undecidable. Note that for example Type families are "artificially" limited to avoid undecidable instances by forbidding certain well-formed programs by default, so allowing a "k-recursive" polymorphic recursion would not be very different from that case, IMHO.
– Bakuriu
1 hour ago
Yes, but I think all extensions to the type systems on top of Haskell2010 make type inference undecidable. Note that for example Type families are "artificially" limited to avoid undecidable instances by forbidding certain well-formed programs by default, so allowing a "k-recursive" polymorphic recursion would not be very different from that case, IMHO.
– Bakuriu
1 hour ago
add a comment |
Thanks for contributing an answer to Stack Overflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f55402733%2fwhy-does-ghc-infer-a-monomorphic-type-here-even-with-monomorphismrestriction-di%23new-answer', 'question_page');
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function ()
StackExchange.helpers.onClickDraftSave('#login-link');
);
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Doesn't the monomorphism restriction apply only to simple bindings anyways (and
w' = fromInteger w'
, being recursive, is not simple)?– Alec
4 hours ago
@Alec possible, but still – why does something like the monomorphism restriction seem to kick in here?
– leftaroundabout
4 hours ago
I'm probably being dense and missing something here, but
fromInteger
has type(Num a) => Integer -> a
, and sincew'
is used as the input tofromInteger
, doesn't that meanInteger
is the only possible type for it? Indeed I'm rather surprised that the version with the polymorphic type signature compiles. (So as I said, probably missing something.)– Robin Zigmond
4 hours ago
@RobinZigmond
Integer
is certainly the only possible monomorphic type forw'
, but asw
demonstrates a polymorphic type is perfectly fine as well. After all, a polymorphic type can be instantiated to a monomorphic one, provided it fulfills the constraints.– leftaroundabout
4 hours ago