![](/i/fill.gif) |
![](/i/fill.gif) |
|
![](/i/fill.gif) |
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
OK, so I know nobody actually cares or anything, but I just "finished"
work on a program that takes a Haskell expression, plus the type
signatures for any free variables mentioned, and figures out what the
type of the expression and all its subexpressions is.
Sounds pretty easy, right? Well let me tell you, it's taken me the
entire week to get it to work properly!
The final program is not especially large or complex, but *getting* to
this point has been a long hard journey. Taking a nontrivial program and
rearranging it while you try out different designs is quite a lot of
work. If I had known in my head exactly how I was going to code this
before I started typing, I could have finished it significantly sooner!
The first major task is to write an expression parser. This is
*drastically* less trivial than it sounds! (Currently my parser
understands only a fraction of Haskell's full syntax. The bare minimum
to parse useful expressions.) And the expression trees are so verbose
that you really *need* a pretty-printer too. Ideally with propper
bracket handling. (You have *no idea* how damned long it took to get the
brackets to work correctly...)
Next, you quickly find that various program passes manfunction if
variable names are not unique. Like, if somebody writes "(\x -> x) (\x
-> x + 1)", those are two different, unrelated local variables which
both just happen to be called "x". So you need to somehow make all the
variable names unique, while correctly respecting the language scoping
rules. This is surprisingly easy to do wrong. (And maddeningly tricky to
track down once you notice it's wrong - if you notice at all!)
Then you're going to need a type unification engine. The basic algorithm
is simple, but there are a large number of minor practical details which
all have to be implemented correctly or you get gibberish. Good luck
testing it! Debugging is even more fun...
Next you need to take the expression and decompose it into a set of
subexpressions and note down their interrelationships. From these, you
can compute a set of type relations which the unification engine then
applies. If unification succeeds, you get a list of type signatures for
every subexpression. If unification fails, the expression is ill-typed.
Or your type checker is buggy!
Ah, but wait! The exact way you decompose the expression and apply the
unification process dictate what result you get. In the process of
crawling through this stuff, I discovered things I never even realised
about Haskell's type system. For example...
(foo 1, foo 'x')
If "foo" is a top-level variable, this expression might be well-typed.
("Might" depending on what type signature foo has, obviously.) However,
if "foo" is a local variable, then the above expression is *guaranteed*
to be ill-typed.
Stop and think about that for a moment: Where a variable is bound
determins whether this expression is well-typed or not. That should tell
you that something pretty subtle is going on here!
I never realised this, but look:
\ foo -> (foo 1, foo 'x')
There is no type which can be assigned to "foo" which will make this
expression acceptable. However, consider this:
foo :: x -> x
bar = (foo 1, foo 'x')
This *is* well-typed. It seems that for each invocation of "foo", the
"x" type variable is allowed to take on a different value. However, in
\ foo -> (foo 1)
the expression's type is going to be "(Int -> y) -> y". Basically here
"foo" is required to have one specific type, and it must be the same
each time it's used.
There's actually a non-standard extension that allows you to write
(\ foo -> (foo 1, foo 'x')) :: forall x. (x -> y) -> (y, y)
The above will now type-check. I think what the magical "forall" keyword
is actually doing is generating a new type variable inside the type
checker each time "foo" is mentioned...
Well, there we are. Now I'm off to go implement the rest of my
program... (Such as, say, making it understand more syntax!)
--
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*
Post a reply to this message
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
Orchid XP v8 wrote:
> Ah, but wait! The exact way you decompose the expression and apply the
> unification process dictate what result you get. In the process of
> crawling through this stuff, I discovered things I never even realised
> about Haskell's type system. For example...
>
> (foo 1, foo 'x')
>
> If "foo" is a top-level variable, this expression might be well-typed.
> ("Might" depending on what type signature foo has, obviously.) However,
> if "foo" is a local variable, then the above expression is *guaranteed*
> to be ill-typed.
>
> Stop and think about that for a moment: Where a variable is bound
> determins whether this expression is well-typed or not. That should tell
> you that something pretty subtle is going on here!
>
> I never realised this, but look:
Awesome. On further investigation, it turns out my understanding of
Haskell's type system is actually incorrect. And, unsurprisingly, my
program is incorrect too; it rejects expressions that it should actually
accept.
Nice to know I understand my own favourit programming language, eh? :-}
--
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*
Post a reply to this message
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
Orchid XP v8 wrote:
> variable names unique, while correctly respecting the language scoping
> rules.
Only surprising if you haven't written LISP code. :-)
Indeed, one of the big improvements in LISP was getting this right (i.e.,
lexical scoping rather than textual scoping, or some such terminology). And
it's still a killer in macros.
Still sounds easier to debug than crashing kernel code on a machine with
insufficient memory to host a debugger or compiler. :-)
--
Darren New, San Diego CA, USA (PST)
"We'd like you to back-port all the changes in 2.0
back to version 1.0."
"We've done that already. We call it 2.0."
Post a reply to this message
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
>> variable names unique, while correctly respecting the language scoping
>> rules.
>
> Only surprising if you haven't written LISP code. :-)
...or a lambda calculus interpretter. :-P
> Still sounds easier to debug than crashing kernel code on a machine with
> insufficient memory to host a debugger or compiler. :-)
Probably, yes.
Haskell really is a PITA to parse. I mean, think about it:
- Whitespace is significant. (No context-free parsing here!)
- There are arbitrary user-defined operators, which arbitrary precedence
and associativity.
Mercifully, there are few language keywords. (There's a lot more than
you think, when you sit down and catelogue them, but it's still nothing
compared to, say, Pascal or C.)
Even so, when a user can define an operator like *&*#*|* and set it to
any precedence or associativity, it's not so easy to produce a parse tree...
Post a reply to this message
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
Orchid XP v8 wrote:
> Awesome. On further investigation, it turns out my understanding of
> Haskell's type system is actually incorrect. And, unsurprisingly, my
> program is incorrect too; it rejects expressions that it should actually
> accept.
Oh look, somebody has produced a helpful T-shirt explaining it all:
http://www.cafepress.com/skicalc.6225368
Isn't that nice?
Post a reply to this message
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
Orchid XP v8 wrote:
> The first major task is to write an expression parser. This is
> *drastically* less trivial than it sounds! (Currently my parser
> understands only a fraction of Haskell's full syntax. The bare minimum
> to parse useful expressions.)
Oh *man*... The more I read into this, the more I discover that Haskell
is way, way more flexible than I thought! o_O
For example, you're allowed to give fixity declarations for local
variables. I thought it was only permitted for top-level variables, but
no, apparently every let-expression can contain fixity declarations and
type signatures. So much for a let-binding just being a list of
variables and what they're bound to. :-P
Post a reply to this message
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
I just implemented a program entitled "Test-Sanity". Arguably, the test
has failed. :-P
(I implemented an internal sanity check routine, and this program runs
it to see what output it produces. But maybe it's creator's sanity is
questionable...)
Post a reply to this message
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
Invisible wrote:
> I just implemented a program entitled "Test-Sanity". Arguably, the test
> has failed. :-P
>
> (I implemented an internal sanity check routine, and this program runs
> it to see what output it produces. But maybe it's creator's sanity is
> questionable...)
Ah, excellent. My sanity checker has a bug.
(Being a moron, I thought that one could determine whether a set of sets
are all disjoint merely by taking the intersection of all of them. DUH!)
Post a reply to this message
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
Invisible wrote:
> Haskell really is a PITA to parse. I mean, think about it:
> - Whitespace is significant. (No context-free parsing here!)
I don't think "context-free" means what you think it means. Whitespace being
significant isn't "context".
> - There are arbitrary user-defined operators, which arbitrary precedence
> and associativity.
But they have to be defined by the user before you use them, so that doesn't
seem hard. Most parsers with more than half a dozen operators (I'm looking
at you, C) have tables defining the precedence and associativity anyway.
> compared to, say, Pascal or C.)
Try Ada.
> Even so, when a user can define an operator like *&*#*|* and set it to
> any precedence or associativity, it's not so easy to produce a parse
> tree...
I think maybe you're doing it wrong.
--
Darren New, San Diego CA, USA (PST)
"We'd like you to back-port all the changes in 2.0
back to version 1.0."
"We've done that already. We call it 2.0."
Post a reply to this message
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
>> Haskell really is a PITA to parse. I mean, think about it:
>> - Whitespace is significant. (No context-free parsing here!)
>
> I don't think "context-free" means what you think it means. Whitespace
> being significant isn't "context".
Indentation is significant. To parse the next line, you must know how
far the current line was indented. Hence, "context".
>> - There are arbitrary user-defined operators, which arbitrary
>> precedence and associativity.
>
> But they have to be defined by the user before you use them, so that
> doesn't seem hard.
No, they can be used *before* they're defined. And they can be defined
in a completely seperate source file too. Which makes me wonder how it's
possible to parse an individual file at all... you'd need to potentially
parse every module it imports to work out the operator precedences!
>> Even so, when a user can define an operator like *&*#*|* and set it to
>> any precedence or associativity, it's not so easy to produce a parse
>> tree...
>
> I think maybe you're doing it wrong.
Heh, *maybe*?
Hey, it's *me* we're talking about there. Of *course* I'm doing to wrong!
--
http://blog.orphi.me.uk/
http://www.zazzle.com/MathematicalOrchid*
Post a reply to this message
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |
|
![](/i/fill.gif) |
| ![](/i/fill.gif) |
|
![](/i/fill.gif) |