Re: [Haskell-cafe] A voyage of undiscovery
Andrew Coppin wrote: That seems simple enough (although problematic to implement). However, the Report seems to say that it matters whether or not the bindings are muturally recursive [but I'm not sure precisely *how* it matters...] Seriously, check out the classic Milner paper. Of languages in the ML tradition, Haskell is actually a bit strange in that it doesn't require the programmer to explicitly annotate recursive functions and recursive groups. That's *very* nice for programmers (since the compiler needs to and can figure it out anyways), though it hides some of the implementation complexity since you need to discover the "implicit" annotations. Polymorphic recursion was one of the big bugbears in the original HM inference algorithm. We can deal with it now, like we can deal with rank-N polymorphism (aka polymorphic lambda-binding) and many other improvements, but it's easiest to start out with the original algorithm when learning everything. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A voyage of undiscovery
Andrew Coppin wrote: Robert Greayer wrote: f0 _ = (foo True, foo 'x') where foo = id is well-typed. Really? That actually works? How interesting... This suggests to me that where-clauses also do strange things to the type system. Not too strange, in fact we need it to do that for local definitions to be helpful at all. The short answer is that let-binding is still polymorphic, whereas lambda-binding (passing in a parameter) is monomorphic. If let-binding were not polymorphic, then we could remove it entirely can just desugar everything into lambda-bindings. You should read this classic paper which introduced Hindley--Milner type inference, Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, August 1978. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.67.5276 -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A voyage of undiscovery
Andrew, That seems simple enough (although problematic to implement). However, the Report seems to say that it matters whether or not the bindings are muturally recursive [but I'm not sure precisely *how* it matters...] It means that functions can only be used monomorphically within their own binding group. (That includes the definition of the function itself: functions cannot be polymorphically recursive. Of course, these restrictions do not apply in case of explicit type signatures. Even if this doesn't all make sense, immediately, it should give you something to google for. ;-)) Cheers, Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A voyage of undiscovery
John Meacham wrote: actually, the rules are pretty straightforward. It doesn't matter where something is bound, just _how_ it is bound. Let-bound names (which includes 'where' and top-level definitions) can be polymorphic. lambda-bound or case-bound names (names bound as an argument to a function or that appear in a pattern) can only be monomorphic. And that's all there is to it. (the monomorphism restriction complicates it a little, but we don't need to worry about that for now) That seems simple enough (although problematic to implement). However, the Report seems to say that it matters whether or not the bindings are muturally recursive [but I'm not sure precisely *how* it matters...] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A voyage of undiscovery
Derek Elkins wrote: The answer to your questions are on the back of this T-shirt. http://www.cafepress.com/skicalc.6225368 Oh... dear God. o_O ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] A voyage of undiscovery
2009/7/17 Andrew Coppin : > I've been working hard this week, and I'm stumbled upon something which is > probably of absolutely no surprise to anybody but me. > > Consider the following expression: > > (foo True, foo 'x') > > Is this expression well-typed? > > Astonishingly, the answer depends on where "foo" is defined. If "foo" is a > local variable, then the above expression is guaranteed to be ill-typed. > However, if we have (for example) > > foo :: x -> x > > as a top-level function, then the above expression becomes well-typed. Some useful reading material: Section 22.7 of the book "Types and Programming Languages" by Benjamin Pierce. The classic paper "Basic Polymorphic Typechecking" by Luca Cardelli: http://lucacardelli.name/Papers/BasicTypechecking.pdf Both of these are very readable introductions to the let-style polymorphism found in the Hindley/Milner type system. Haskell's type system is essentially an elaboration of that idea. Pierce's book shows how to achieve let-polymorphism by inlining non-recursive let bindings during type checking/inference, which is a nice way to understand what is going on. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A voyage of undiscovery
On Thu, Jul 16, 2009 at 08:52:40PM +0100, Andrew Coppin wrote:
> Ross Mellgren wrote:
>> It's not where -- let also works
>>
>> Prelude> let { foo x = x } in (foo 1, foo True)
>> (1,True)
>
> Awesome. So by attempting to implement Haskell's type system, I have
> discovered that I actually don't understand Haskell's type system. Who'd
> have thought it?
>
> Clearly I must go consult the Report and check precisely what the rules
> are...
actually, the rules are pretty straightforward. It doesn't matter where
something is bound, just _how_ it is bound. Let-bound names (which
includes 'where' and top-level definitions) can be polymorphic.
lambda-bound or case-bound names (names bound as an argument to a
function or that appear in a pattern) can only be monomorphic. And
that's all there is to it. (the monomorphism restriction complicates it
a little, but we don't need to worry about that for now)
As an extension, ghc and jhc allow arguments and case bound variables to
be polymorphic but only when explicitly declared so by a user supplied
type annotation. (the exact rules for what 'explicitly declared' means
can be a little complicated when formalized, but they match up enough
with intuition that it isn't a problem in practice). They will never
infer such a type on their own.
John
--
John Meacham - ⑆repetae.net⑆john⑈ - http://notanumber.net/
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A voyage of undiscovery
Is "everything" an acceptable answer?
-Ross
On Jul 16, 2009, at 6:38 PM, Derek Elkins wrote:
On Thu, Jul 16, 2009 at 2:52 PM, Andrew
Coppin wrote:
Ross Mellgren wrote:
It's not where -- let also works
Prelude> let { foo x = x } in (foo 1, foo True)
(1,True)
Awesome. So by attempting to implement Haskell's type system, I have
discovered that I actually don't understand Haskell's type system.
Who'd
have thought it?
Clearly I must go consult the Report and check precisely what the
rules
are...
The answer to your questions are on the back of this T-shirt.
http://www.cafepress.com/skicalc.6225368
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A voyage of undiscovery
On Thu, Jul 16, 2009 at 2:52 PM, Andrew
Coppin wrote:
> Ross Mellgren wrote:
>>
>> It's not where -- let also works
>>
>> Prelude> let { foo x = x } in (foo 1, foo True)
>> (1,True)
>
> Awesome. So by attempting to implement Haskell's type system, I have
> discovered that I actually don't understand Haskell's type system. Who'd
> have thought it?
>
> Clearly I must go consult the Report and check precisely what the rules
> are...
The answer to your questions are on the back of this T-shirt.
http://www.cafepress.com/skicalc.6225368
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A voyage of undiscovery
Andrew Coppin wrote: Awesome. So by attempting to implement Haskell's type system, I have discovered that I actually don't understand Haskell's type system. Who'd have thought it? Clearly I must go consult the Report and check precisely what the rules are... I just read section 4.5 of the Haskell 98 Report. Ouch! >_< I knew I'd be sorry I asked... Time for bed, I think! ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A voyage of undiscovery
Ross Mellgren wrote:
It's not where -- let also works
Prelude> let { foo x = x } in (foo 1, foo True)
(1,True)
Awesome. So by attempting to implement Haskell's type system, I have
discovered that I actually don't understand Haskell's type system. Who'd
have thought it?
Clearly I must go consult the Report and check precisely what the rules
are...
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A voyage of undiscovery
On Thu, Jul 16, 2009 at 12:40 PM, Andrew Coppin wrote: > Robert Greayer wrote: > >> f0 _ = (foo True, foo 'x') where foo = id >> >> is well-typed. >> >> > > Really? That actually works? How interesting... This suggests to me that > where-clauses also do strange things to the type system. You could think of it that way. You mentioned GADTs in your OP. Well, it turns out GADTs often do not play nicely with where/let and it happens to all be related. As I understand it, functions bind their parameters monomorphically and let/where bind things polymorphically. And then we have the misfeature known as the monomorphism restriction which adds special cases. > > whereas >> >> f1 foo = (foo True, foo 'x') >> >> requires 'foo' to be polymorphic in its first argument. This does >> require a higher rank type, which can't be inferred: >> >> You could type f1 as >> f1 :: (forall a . a -> a) -> (Bool, Char) >> >> and apply it to 'id'. >> >> Or you could type it as something like: >> f1 :: (forall a . a -> ()) -> ((),()) >> >> and apply it to 'const ()' >> > > ...all of which is beyond Haskell-98, which is what I am limiting myself to > at present. > > (Actually, even that is a lie. I don't have type-classes yet...) Congrats on the type inference engine you're writing. It's on my list of things to do, and I was even reading up on TaPL a month or two back, but I put it down and haven't picked it up again yet. I think writing one would help flush out my understand of all this stuff. Jason ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A voyage of undiscovery
It's not where -- let also works
let { foo Prelude> let { foo x = x } in (foo 1, foo True)
(1,True)
Can you send the code you're trying that doesn't work?
-Ross
On Jul 16, 2009, at 3:40 PM, Andrew Coppin wrote:
Robert Greayer wrote:
f0 _ = (foo True, foo 'x') where foo = id
is well-typed.
Really? That actually works? How interesting... This suggests to me
that where-clauses also do strange things to the type system.
whereas
f1 foo = (foo True, foo 'x')
requires 'foo' to be polymorphic in its first argument. This does
require a higher rank type, which can't be inferred:
You could type f1 as
f1 :: (forall a . a -> a) -> (Bool, Char)
and apply it to 'id'.
Or you could type it as something like:
f1 :: (forall a . a -> ()) -> ((),())
and apply it to 'const ()'
...all of which is beyond Haskell-98, which is what I am limiting
myself to at present.
(Actually, even that is a lie. I don't have type-classes yet...)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A voyage of undiscovery
Robert Greayer wrote: f0 _ = (foo True, foo 'x') where foo = id is well-typed. Really? That actually works? How interesting... This suggests to me that where-clauses also do strange things to the type system. whereas f1 foo = (foo True, foo 'x') requires 'foo' to be polymorphic in its first argument. This does require a higher rank type, which can't be inferred: You could type f1 as f1 :: (forall a . a -> a) -> (Bool, Char) and apply it to 'id'. Or you could type it as something like: f1 :: (forall a . a -> ()) -> ((),()) and apply it to 'const ()' ...all of which is beyond Haskell-98, which is what I am limiting myself to at present. (Actually, even that is a lie. I don't have type-classes yet...) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A voyage of undiscovery
On Thu, Jul 16, 2009 at 2:34 PM, Andrew Coppin wrote: > I've been working hard this week, and I'm stumbled upon something which is > probably of absolutely no surprise to anybody but me. > > Consider the following expression: > > (foo True, foo 'x') > > Is this expression well-typed? > > Astonishingly, the answer depends on where "foo" is defined. If "foo" is a > local variable, then the above expression is guaranteed to be ill-typed. This isn't completely accurate: f0 _ = (foo True, foo 'x') where foo = id is well-typed. whereas f1 foo = (foo True, foo 'x') requires 'foo' to be polymorphic in its first argument. This does require a higher rank type, which can't be inferred: You could type f1 as f1 :: (forall a . a -> a) -> (Bool, Char) and apply it to 'id'. Or you could type it as something like: f1 :: (forall a . a -> ()) -> ((),()) and apply it to 'const ()' ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] A voyage of undiscovery
Consider the following expression: (foo True, foo 'x') Is this expression well-typed? Astonishingly, the answer depends on where "foo" is defined. If "foo" is a local variable, then the above expression is guaranteed to be ill-typed. However, if we have (for example) That's not true: main = let foo x = x in print (foo True, foo 'x') works like a charm. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] A voyage of undiscovery
I've been working hard this week, and I'm stumbled upon something which is probably of absolutely no surprise to anybody but me. Consider the following expression: (foo True, foo 'x') Is this expression well-typed? Astonishingly, the answer depends on where "foo" is defined. If "foo" is a local variable, then the above expression is guaranteed to be ill-typed. However, if we have (for example) foo :: x -> x as a top-level function, then the above expression becomes well-typed. I had never ever noticed this fact before. I'm still trying to bend my mind around exactly why it happens. As best as I can tell, top-level functions (and value constructors, for that matter) seem to get a "new" set of type variables each time they're used, but local variables each get a single type variable, so every mention of a local variable must be of the exact same type. Could this be what GHC's weird "forall" syntax is about? Does "forall x." mean that "x" gets replaced with a unique type variable each time? It's an interesting hypothesis... Anyway, not that anybody is likely to care, but I've just spent an entire week writing a program which can type-check simple Haskell expressions. As in, you type in an expression and give types to any free variables it involves (including value constructor functions), and it tells you the type of the expression and all its subexpressions. (Or tells you that it's ill-typed.) It turns out that this is radically less trivial than you'd imagine. (The ramblings above being just one of the issues I blundered into. Others include the subtleties of writing an expression parser, building a pretty-printer with bracketing that works correctly, and the fact that expression processing malfunctions horribly if you don't make all the variable names unique first...) Other issues were mostly related to the difficulty of constantly refactoring code because you're not quite sure what you're trying to do or how you're trying to do it. (And obscure type checker warnings about GADTs...) Well there we are. I don't suppose anybody will be overly impressed, but I'm glad to have finally got it to work. Now, if it could parse more than 10% of Haskell's syntax sugar, it might even be useful for something... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
