gmane.comp.lang.haskell.cafe

Neil Mitchell | 27 Aug 22:08

Re: Compiler's bane

Hi

> I'm writing a simple interpretter for a small extended-lambda-calculus sort
> of language. And I'd just like to say... RECURSIVE LET-BINDS! GAAAAH!!! >_<

Agreed 

> To illustrate:
>
>  let x = f x; y = 5 in x y
>
> A simple-minded interpretter might try to replace every occurrance of "x"
> with "f x". This yields
>
>  let y = 5 in (f x) y

That's wrong, its a two step transformation. You just substitute all
occurances of x for f x:

let x = f (f x); y = 5 in (f x) y

For the case let x = 5 in x, you do the same thing:

let x = 5 in 5

Now as a second step you hoover up unused let bindings and disguard:

5

You seem to be combining the substitution and the removing of dead let

(Continue reading)

headers

Andrew Coppin | 29 Aug 21:56

Re: Compiler's bane

Neil Mitchell wrote:
> Hi
>
>   
>> I'm writing a simple interpretter for a small extended-lambda-calculus sort
>> of language. And I'd just like to say... RECURSIVE LET-BINDS! GAAAAH!!! >_<
>>     
>
> Agreed 
>   

I'm glad it's not just me! 

(Oleg cat sez: "see, yr type problum not so hard".)

>> To illustrate:
>>
>>  let x = f x; y = 5 in x y
>>
>> A simple-minded interpretter might try to replace every occurrance of "x"
>> with "f x". This yields
>>
>>  let y = 5 in (f x) y
>>     
>
> That's wrong, its a two step transformation. You just substitute all
> occurances of x for f x:
>
> let x = f (f x); y = 5 in (f x) y
>

(Continue reading)

headers

Jonathan Cast | 29 Aug 22:12

Re: Compiler's bane

On Fri, 2008-08-29 at 20:56 +0100, Andrew Coppin wrote:
> Neil Mitchell wrote:
> > Hi
> >
> >   
> >> I'm writing a simple interpretter for a small extended-lambda-calculus sort
> >> of language. And I'd just like to say... RECURSIVE LET-BINDS! GAAAAH!!! >_<
> >>     
> >
> > Agreed 
> >   
> 
> I'm glad it's not just me! 
> 
> (Oleg cat sez: "see, yr type problum not so hard".)
> 
> >> To illustrate:
> >>
> >>  let x = f x; y = 5 in x y
> >>
> >> A simple-minded interpretter might try to replace every occurrance of "x"
> >> with "f x". This yields
> >>
> >>  let y = 5 in (f x) y
> >>     
> >
> > That's wrong, its a two step transformation. You just substitute all
> > occurances of x for f x:
> >
> > let x = f (f x); y = 5 in (f x) y

(Continue reading)

headers

Conor McBride | 29 Aug 22:48

Re: Compiler's bane

Hi

On 29 Aug 2008, at 21:12, Jonathan Cast wrote:

>
> If you want to avoid infinite normal forms (or just plain lack of  
> normal
> forms, as in let x = x in x or (\x -> x x) (\ x -> x x)), you need to
> follow three rules:
>
> 1) Static typing

With you there.

> 2) No value recursion

Mostly with you: might allow productive corecursion
computing only on demand.

> 3) If you allow data types, no recursive data types

I can think of a few Turing incomplete languages with
(co)recursive data types, so

> Otherwise, your language will be Turing-complete,

seems suspect to me.

It's quite possible to identify a total fragment of
Haskell, eg, by seeing which of your Haskell programs

(Continue reading)

headers

Jonathan Cast | 29 Aug 22:49

Re: Compiler's bane

On Fri, 2008-08-29 at 21:48 +0100, Conor McBride wrote:
> Hi
> 
> On 29 Aug 2008, at 21:12, Jonathan Cast wrote:
> 
> >
> > If you want to avoid infinite normal forms (or just plain lack of  
> > normal
> > forms, as in let x = x in x or (\x -> x x) (\ x -> x x)), you need to
> > follow three rules:
> >
> > 1) Static typing
> 
> With you there.
> 
> > 2) No value recursion
> 
> Mostly with you: might allow productive corecursion
> computing only on demand.
> 
> > 3) If you allow data types, no recursive data types
> 
> I can think of a few Turing incomplete languages with
> (co)recursive data types, so

> > Otherwise, your language will be Turing-complete,
> 
> seems suspect to me.

OK.  If you have any of

(Continue reading)

headers

Andrew Coppin | 31 Aug 09:46

Re: Compiler's bane

Jonathan Cast wrote:
> On Fri, 2008-08-29 at 20:56 +0100, Andrew Coppin wrote:
>   
>> I've been playing with this today, and no matter what rules I come up 
>> with, it seems to be ridiculously easy to put the interpretter into an 
>> infinite loop from which it will never escape. Is there any way to know 
>> which binds are "worth" expanding and which ones aren't? (I have a 
>> sinking feeling this might be equivilent to the Halting Problem...)
>>
>> For example, if you have "let x = f y; y = g x in x" then since all the 
>> functions are free variables, there's really nothing much "useful" you 
>> can do to simplify this any further. However, my interpretter merrily 
>> goes into an endless loop building a huge expression like "f (g (f (g (f 
>> (g..." Is it possible to avoid this?
>>     
>
> If you want to avoid infinite normal forms (or just plain lack of normal
> forms, as in let x = x in x or (\x -> x x) (\ x -> x x)), you need to
> follow three rules:
>
> 1) Static typing
> 2) No value recursion
> 3) If you allow data types, no recursive data types
>
> Otherwise, your language will be Turing-complete, so yes, trying to
> determine ahead of time if even a HNF exists will be the halting
> problem.
>
> If you really want to write a general-purpose evaluator, then infinite
> normal forms may not be an issue, as long as they are generated lazily,

(Continue reading)

headers

Ryan Ingram | 31 Aug 11:52

Re: Compiler's bane

On Sun, Aug 31, 2008 at 12:46 AM, Andrew Coppin
<andrewcoppin <at> btinternet.com> wrote:
> Right. So if I have, say, the factorial function defined using the Y
> combinator, there's no way to stop the interpretter expanding an infinite
> number of copies of Y, even though in theory the factorial function should
> terminate?

Well, this is exactly what ghci is doing; you just have to choose an
evaluation order that makes sense.

Lets consider a simple translation for recursive lets:
> let x = exp1 in exp2
(where x may be free in exp1 and/or exp2)

Here's a simple translation into lambda-calculus:
> (\x. exp2) (y (\x. exp1))

(Of course, this representation for let can lose sharing; without
knowing what you have or your goals I don't know if you care).

Now, you just have to choose a y-combinator that makes sense for your
evaluation order.  If you do normal-order evaluation like Haskell
("non-strict"), this Y should work for you:

y = \f. (\x. f (x x)) (\x. f (x x))

> Oh well, I guess I'll just have to live with that one. Maybe I can make the
> binding to expand user-selectable or something...

Now, if you are eagerly-expanding the entire expression, trying to get

(Continue reading)

headers

Andrew Coppin | 31 Aug 18:29

Re: Compiler's bane

Ryan Ingram wrote:
> On Sun, Aug 31, 2008 at 12:46 AM, Andrew Coppin
> <andrewcoppin <at> btinternet.com> wrote:
>   
>> Right. So if I have, say, the factorial function defined using the Y
>> combinator, there's no way to stop the interpretter expanding an infinite
>> number of copies of Y, even though in theory the factorial function should
>> terminate?
>>     
>
> Well, this is exactly what ghci is doing; you just have to choose an
> evaluation order that makes sense.
>
> Lets consider a simple translation for recursive lets:
>   
>> let x = exp1 in exp2
>>     
> (where x may be free in exp1 and/or exp2)
>
> Here's a simple translation into lambda-calculus:
>   
>> (\x. exp2) (y (\x. exp1))
>>     
>
> (Of course, this representation for let can lose sharing; without
> knowing what you have or your goals I don't know if you care).
>
> Now, you just have to choose a y-combinator that makes sense for your
> evaluation order.  If you do normal-order evaluation like Haskell
> ("non-strict"), this Y should work for you:

(Continue reading)

headers

Jonathan Cast | 31 Aug 20:08

Re: Compiler's bane

On Sun, 2008-08-31 at 17:29 +0100, Andrew Coppin wrote:
> Ryan Ingram wrote:
> > On Sun, Aug 31, 2008 at 12:46 AM, Andrew Coppin
> > <andrewcoppin <at> btinternet.com> wrote:
> >   
> >> Right. So if I have, say, the factorial function defined using the Y
> >> combinator, there's no way to stop the interpretter expanding an infinite
> >> number of copies of Y, even though in theory the factorial function should
> >> terminate?
> >>     
> >
> > Well, this is exactly what ghci is doing; you just have to choose an
> > evaluation order that makes sense.
> >
> > Lets consider a simple translation for recursive lets:
> >   
> >> let x = exp1 in exp2
> >>     
> > (where x may be free in exp1 and/or exp2)
> >
> > Here's a simple translation into lambda-calculus:
> >   
> >> (\x. exp2) (y (\x. exp1))
> >>     
> >
> > (Of course, this representation for let can lose sharing; without
> > knowing what you have or your goals I don't know if you care).
> >
> > Now, you just have to choose a y-combinator that makes sense for your
> > evaluation order.  If you do normal-order evaluation like Haskell

(Continue reading)

headers

Ryan Ingram | 31 Aug 20:10

Re: Compiler's bane

On Sun, Aug 31, 2008 at 9:29 AM, Andrew Coppin
<andrewcoppin <at> btinternet.com> wrote:
> All of this strongly suggests that if you execute things in the correct
> order, you can arrange it so that expressions that have a normal form will
> be evaluated to it. But how to decide the correct evaluation order? For the
> plain lambda calculus, IIRC you just have to execute the left-most,
> outer-most redex every time and it'll work. For a language with let-binds,
> it is unclear to me how to proceed...

What are you trying to get from the "let" binding?  Sharing?

The usual idea is that "let" represents heap allocation, and you
evaluate the leftmost-outermost redex as usual, doing let substitution
only when necessary to continue evaluation, and garbage-collecting
bindings that no longer refer to variables in the current computation.
 You also make lambda-expressions create let-bindings during
substitution to maximize sharing.

Here's an example of how an interpreter could work:

let fact_acc = \n x. (== n 0) x (fact_acc (- n 1) (* n x))
in fact_acc 3 1

The "top-level" redex is a let bind that is already in WHNF; if it
wasn't, you continue evaluation inside of it.  So instead you
substitute and lose sharing because there are no other options.

I'm going to leave all previous "lets" as "..." in this evaluation to
save typing:

(Continue reading)

headers

Andrew Coppin | 31 Aug 21:14

Re: Compiler's bane

Ryan Ingram wrote:
> What are you trying to get from the "let" binding?  Sharing?
>   

Convinience.

  let x = foo in bar

is so much easier to write than

  (\x -> bar) foo

when foo and/or bar is large.

Trouble is, as soon as you allow let-bindings, some clever person is 
going to start writing recursive ones. And actually, that's a useful 
thing to be able to do, but it makes figuring out the technical 
details... rather nontrivial. (Seriously, I had no idea I was going to 
get into this much trouble!)
> The usual idea is that "let" represents heap allocation, and you
> evaluate the leftmost-outermost redex as usual, doing let substitution
> only when necessary to continue evaluation, and garbage-collecting
> bindings that no longer refer to variables in the current computation

Right. So ignore the let-bindings unless the redex of interest is a 
let-bound variable? That sounds reasonably easy...

headers

Jeremy Apthorp | 31 Aug 23:33

Re: Compiler's bane

2008/9/1 Andrew Coppin <andrewcoppin <at> btinternet.com>:
> Ryan Ingram wrote:
>>
>> What are you trying to get from the "let" binding?  Sharing?
>>
>
> Convinience.
>
>  let x = foo in bar
>
> is so much easier to write than
>
>  (\x -> bar) foo
>
> when foo and/or bar is large.
>
> Trouble is, as soon as you allow let-bindings, some clever person is going
> to start writing recursive ones. And actually, that's a useful thing to be
> able to do, but it makes figuring out the technical details... rather
> nontrivial. (Seriously, I had no idea I was going to get into this much
> trouble!)

I'm confused -- why is this different to having recursive top-level bindings?

Jeremy

headers

Andrew Coppin | 1 Sep 20:44

Re: Compiler's bane

Jeremy Apthorp wrote:
> 2008/9/1 Andrew Coppin <andrewcoppin <at> btinternet.com>:
>   
>> Trouble is, as soon as you allow let-bindings, some clever person is going
>> to start writing recursive ones. And actually, that's a useful thing to be
>> able to do, but it makes figuring out the technical details... rather
>> nontrivial. (Seriously, I had no idea I was going to get into this much
>> trouble!)
>>     
>
> I'm confused -- why is this different to having recursive top-level bindings?
>   

It isn't different - and if my interpretter ever has top-level bindings, 
it'll introduce all the same problems. :-S

headers

Andrew Coppin | 1 Sep 20:47

Re: Compiler's bane

Here is a *much* bigger problem: How do you check that an interpretter 
is correct??

You can't very easily write a QuickCheck property that will generate 
every possible valid expression and then check that the output of the 
interpretter is formally equivilent. The QuickCheck property would be a 
second copy of the interpretter, which proves nothing!

Any hints? Just how *do* you check something large like this?

I wonder - how do the GHC developers check that GHC works properly? (I 
guess by compiling stuff and running it... It's a bit harder to check 
that a lambda interpretter is working right.)

headers

Brandon S. Allbery KF8NH | 1 Sep 21:38

Re: Compiler's bane

On 2008 Sep 1, at 14:47, Andrew Coppin wrote:
> I wonder - how do the GHC developers check that GHC works properly?  
> (I guess by compiling stuff and running it... It's a bit harder to  
> check that a lambda interpretter is working right.)

GHC has a comprehensive test suite (not included in the source tarball  
or the default checkout but easily checked out atop GHC).

--

-- 
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery <at> kf8nh.com
system administrator [openafs,heimdal,too many hats] allbery <at> ece.cmu.edu
electrical and computer engineering, carnegie mellon university    KF8NH

headers

Andrew Coppin | 3 Sep 20:36

Re: Compiler's bane

Brandon S. Allbery KF8NH wrote:
> On 2008 Sep 1, at 14:47, Andrew Coppin wrote:
>> I wonder - how do the GHC developers check that GHC works properly? 
>> (I guess by compiling stuff and running it... It's a bit harder to 
>> check that a lambda interpretter is working right.)
>
> GHC has a comprehensive test suite (not included in the source tarball 
> or the default checkout but easily checked out atop GHC).

I'm sure a large, complex product like GHC would have a large test 
suite. I was asking how it works. 

Since GHC actually transforms Haskell to machine code in several stages, 
I presume each one can be checked independently, which probably makes 
things easier. But I bet the GHC developers don't have any way to just 
automatically build 1,000 random test cases and check that the compiler 
"works" for those...

headers

Tillmann Rendel | 2 Sep 02:06

Re: Compiler's bane

Andrew Coppin wrote:
> Here is a *much* bigger problem: How do you check that an interpretter 
> is correct??

Before checking for correctness, you have to define correctness. What is 
the specification of your interpreter?

> You can't very easily write a QuickCheck property that will generate 
> every possible valid expression and then check that the output of the 
> interpretter is formally equivilent. The QuickCheck property would be a 
> second copy of the interpretter, which proves nothing!

Well, if you have two *different* interpreters, that would at least 
reassure you somewhat. Consider a naive substituation-based interpreter 
and a clever environment-based interpreter. The former is often easier 
to write and easier to get correct, and the latter is often what you 
want in the end.

Since you seem to be implementing a standard language, you could use an 
existing implementation to check against. many lambda calculus style 
languages can easily be transformed into scheme, for example.

> Any hints? Just how *do* you check something large like this?

You could write a lot of test cases, calculating the correct answers by 
hand.

You could check that during evaluation, you have always wellformed terms 
(e.g. evaluation does not introduce new free variables). You could even 
check that after evaluation stops, you have indeed a normal form.

(Continue reading)

headers

Brandon S. Allbery KF8NH | 2 Sep 05:18

Re: Compiler's bane

On 2008 Sep 1, at 20:06, Tillmann Rendel wrote:
> Andrew Coppin wrote:
>> Any hints? Just how *do* you check something large like this?
>
> You could write a lot of test cases, calculating the correct answers  
> by hand.
>
> You could check that during evaluation, you have always wellformed  
> terms (e.g. evaluation does not introduce new free variables). You  
> could even check that after evaluation stops, you have indeed a  
> normal form.
>
> You could try to check the components of your interpreter (e.g.  
> environment lookup, term substituation, simplification) independently.

You can define a set of valid transformations, have the interpreter  
log each transformation, and verify that all are correct (that is,  
that both the transformation and the logged result are correct.

This assumes the interpreter can be resolved down to a sufficiently  
simple set of transformations; if not, you're right back at having the  
tester being the interpreter itself.  Note that you don't check if the  
transformation plan for the program matches a specified list, just  
that all transformations are correct.  (Just remember that "logic is  
an organized way of going wrong with confidence.")

--

-- 
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery <at> kf8nh.com
system administrator [openafs,heimdal,too many hats] allbery <at> ece.cmu.edu
electrical and computer engineering, carnegie mellon university    KF8NH

(Continue reading)

headers

Andrew Coppin | 3 Sep 20:34

Re: Compiler's bane

Brandon S. Allbery KF8NH wrote:
> You can define a set of valid transformations, have the interpreter 
> log each transformation, and verify that all are correct (that is, 
> that both the transformation and the logged result are correct.
>
> This assumes the interpreter can be resolved down to a sufficiently 
> simple set of transformations; if not, you're right back at having the 
> tester being the interpreter itself.  Note that you don't check if the 
> transformation plan for the program matches a specified list, just 
> that all transformations are correct.  (Just remember that "logic is 
> an organized way of going wrong with confidence.")

The amusing (?) part is that the interpretter itself is essentially 
quite simple. I've implemented it several times before now. But what I'm 
trying to do it make it print out elaborately formatted execution traces 
so that a human user can observe how execution proceeds. This transforms 
an essentially simple algorithm into something quite nausiatingly 
complex, with many subtle bugs and issues.

Still, I guess it's not news to anybody that proof-of-concept programs 
are much easier that real-world implementations.

One thing I could do is have QuickCheck build arbitrary expressions, run 
those through the pretty printer, and then run the result back through 
the parser and check that I get the same expression. Can anybody tell me 
how to get QuickCheck to build arbitrary expressions though? Let's say I had

  data Expression = Var String | Apply Expression Expression | Lambda 
String Expression

(Continue reading)

headers

Ryan Ingram | 3 Sep 23:54

Re: Compiler's bane

On Wed, Sep 3, 2008 at 11:34 AM, Andrew Coppin
<andrewcoppin <at> btinternet.com> wrote:
>  data Expression = Var String | Apply Expression Expression | Lambda String
> Expression
>
> How would you go about building random expression trees?

It's pretty simple, I think.  Keep an environment of variable names
that are in enclosing lambdas, then randomly choose Apply/Lambda/Var,
ignoring Var if the environment is empty, and with Lambda adding to
the environment of its subexpression.

I suggest

type ExpGen = ReaderT [String] Gen

arbExp :: ExpGen Expression
-- exercise for the reader

instance Arbitrary Expression where
    arbitrary = runReaderT arbExp []
    coarbitrary = coarbExp

coarbExp (Var s)      = variant 0 . coarbitrary s
coarbExp (Apply a b)  = variant 1 . coarbitrary a . coarbitrary b
coarbExp (Lambda s e) = variant 2 . coarbitrary s . coarbitrary e

-- Also, apparently there is no default Arbitrary instance for strings, so...
instance Arbitrary Char where
  arbitrary   = elements "abcdefghijklmnopqrstuvwxyz_"

(Continue reading)

headers

Andrew Coppin | 4 Sep 19:41

Re: Compiler's bane

Ryan Ingram wrote:
> It's pretty simple, I think.
>
> type ExpGen = ReaderT [String] Gen
>
> arbExp :: ExpGen Expression
> -- exercise for the reader
>
> instance Arbitrary Expression where
>     arbitrary = runReaderT arbExp []
>     coarbitrary = coarbExp
>
> coarbExp (Var s)      = variant 0 . coarbitrary s
> coarbExp (Apply a b)  = variant 1 . coarbitrary a . coarbitrary b
> coarbExp (Lambda s e) = variant 2 . coarbitrary s . coarbitrary e
>
> instance Arbitrary Char where
>   arbitrary   = elements "abcdefghijklmnopqrstuvwxyz_"
>   coarbitrary = coarbitrary . fromEnum
>   

o_O

I love the way other people have wildly different ideas of "simple" than 
me. I'm staring at this and completely failing to comprehend it. (But 
then, anything with "co" in the name generally makes little sense to 
me...) Why on earth would you need a reader monad? Surely if you want to 
add bound variables and then later query what variables are bound, you'd 
want a state monad? Hmm, I'm completely lost here.

(Continue reading)

headers

Jonathan Cast | 4 Sep 19:50

Re: Compiler's bane

On Thu, 2008-09-04 at 18:41 +0100, Andrew Coppin wrote:
> Ryan Ingram wrote:
> > It's pretty simple, I think.
> >
> > type ExpGen = ReaderT [String] Gen
> >
> > arbExp :: ExpGen Expression
> > -- exercise for the reader
> >
> > instance Arbitrary Expression where
> >     arbitrary = runReaderT arbExp []
> >     coarbitrary = coarbExp
> >
> > coarbExp (Var s)      = variant 0 . coarbitrary s
> > coarbExp (Apply a b)  = variant 1 . coarbitrary a . coarbitrary b
> > coarbExp (Lambda s e) = variant 2 . coarbitrary s . coarbitrary e
> >
> > instance Arbitrary Char where
> >   arbitrary   = elements "abcdefghijklmnopqrstuvwxyz_"
> >   coarbitrary = coarbitrary . fromEnum
> >   
> 
> o_O
> 
> I love the way other people have wildly different ideas of "simple" than 
> me. I'm staring at this and completely failing to comprehend it. (But 
> then, anything with "co" in the name generally makes little sense to 
> me...) Why on earth would you need a reader monad? Surely if you want to 
> add bound variables and then later query what variables are bound, you'd 
> want a state monad? Hmm, I'm completely lost here.

(Continue reading)

headers

Brandon S. Allbery KF8NH | 4 Sep 20:27

Re: Compiler's bane

On Sep 4, 2008, at 13:41 , Andrew Coppin wrote:
> Ryan Ingram wrote:
>> It's pretty simple, I think.
>>
>> type ExpGen = ReaderT [String] Gen
>>
>> arbExp :: ExpGen Expression
>> -- exercise for the reader
>>
>> instance Arbitrary Expression where
>>    arbitrary = runReaderT arbExp []
>>    coarbitrary = coarbExp
>>
>> coarbExp (Var s)      = variant 0 . coarbitrary s
>> coarbExp (Apply a b)  = variant 1 . coarbitrary a . coarbitrary b
>> coarbExp (Lambda s e) = variant 2 . coarbitrary s . coarbitrary e
>>
>> instance Arbitrary Char where
>>  arbitrary   = elements "abcdefghijklmnopqrstuvwxyz_"
>>  coarbitrary = coarbitrary . fromEnum
>>
>
> o_O
>
> I love the way other people have wildly different ideas of "simple"  
> than me. I'm staring at this and completely failing to comprehend  
> it. (But then, anything with "co" in the name generally makes little  
> sense to me...) Why on earth would you need a reader monad? Surely  
> if you want to add bound variables and then later query what  
> variables are bound, you'd want a state monad? Hmm, I'm completely

(Continue reading)

headers

Ryan Ingram | 4 Sep 21:57

Re: Compiler's bane

On Thu, Sep 4, 2008 at 10:41 AM, Andrew Coppin
<andrewcoppin <at> btinternet.com> wrote:
> I love the way other people have wildly different ideas of "simple" than me.
> I'm staring at this and completely failing to comprehend it. (But then,
> anything with "co" in the name generally makes little sense to me...) Why on
> earth would you need a reader monad? Surely if you want to add bound
> variables and then later query what variables are bound, you'd want a state
> monad? Hmm, I'm completely lost here.

Other people have already covered the reader vs. state issue; but to
sum up, this is a state monad, but the state can only be mutated in
sub-expressions, not in future expressions.

In my quick implementation, the branch of arbExp that makes a
lambda-expression looks something like this:

> do
>    -- get a new variable name
>    v <- lift arbitrary
>    -- construct a new expression that may use v as a variable
>    e <- local (v:) arbExp
>    -- return the new expression
>    return (Lambda v e)

As to all the crazy "co" stuff, it's just an implementation detail for
QuickCheck.  It took me a while figure out what was actually going on,
but the implementation is basically just boilerplate at this point.  A
simpler implementation is

> coarbitrary _ = id

(Continue reading)

headers

Brandon S. Allbery KF8NH | 4 Sep 00:25

Re: Compiler's bane

On 2008 Sep 3, at 14:34, Andrew Coppin wrote:
> Brandon S. Allbery KF8NH wrote:
>> You can define a set of valid transformations, have the interpreter  
>> log each transformation, and verify that all are correct (that is,  
>> that both the transformation and the logged result are correct.
>>
>> This assumes the interpreter can be resolved down to a sufficiently  
>> simple set of transformations; if not, you're right back at having  
>> the tester being the interpreter itself.  Note that you don't check  
>> if the transformation plan for the program matches a specified  
>> list, just that all transformations are correct.  (Just remember  
>> that "logic is an organized way of going wrong with confidence.")
>
> The amusing (?) part is that the interpretter itself is essentially  
> quite simple. I've implemented it several times before now. But what  
> I'm trying to do it make it print out elaborately formatted  
> execution traces so that a human user can observe how execution  
> proceeds. This transforms an essentially simple algorithm into  
> something quite nausiatingly complex, with many subtle bugs and  
> issues.

This seems odd to me:  I would expect to wrap a WriterT around it, log  
unformatted actions there, and dump it to a file at the end to be read  
by an analyzer tool which can optionally reformat the log to be human- 
readable.

--

-- 
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery <at> kf8nh.com
system administrator [openafs,heimdal,too many hats] allbery <at> ece.cmu.edu
electrical and computer engineering, carnegie mellon university    KF8NH

(Continue reading)

headers

Andrew Coppin | 4 Sep 19:37

Re: Compiler's bane

Brandon S. Allbery KF8NH wrote:
> On 2008 Sep 3, at 14:34, Andrew Coppin wrote:
>> The amusing (?) part is that the interpretter itself is essentially 
>> quite simple. I've implemented it several times before now. But what 
>> I'm trying to do it make it print out elaborately formatted execution 
>> traces so that a human user can observe how execution proceeds. This 
>> transforms an essentially simple algorithm into something quite 
>> nausiatingly complex, with many subtle bugs and issues.
>
> This seems odd to me:  I would expect to wrap a WriterT around it, log 
> unformatted actions there, and dump it to a file at the end to be read 
> by an analyzer tool which can optionally reformat the log to be 
> human-readable.

Well actually, the interpretter itself takes an expression and returns a 
large, complex data structure representing the reduction sequence. Then 
a second function takes the reduction sequence and transforms it into a 
target-neutral markup structure. Finally, one of several rendering 
backends transforms this into something displayable - text, HTML, LaTeX, 
whatever. There are no monads involved. Anywhere.

Actually, that's not completely true. The interpretter takes a set of 
transformation rules as an argument, and attempts to apply each rule in 
sequence, and then recursively over all subexpressions. The logic for 
this makes extensive use of the Maybe monad. (I spent ages looking for a 
function Maybe x -> Maybe x -> Maybe x that would keep Just and throw 
away Nothing, rather than (>>=) which does the opposite. Eventually I 
discovered that this is actually mplus. It wasn't easy...)

The basic interpretter is just one function, that does a little pattern

(Continue reading)

headers

John Meacham | 27 Aug 22:16

Re: Compiler's bane

On Wed, Aug 27, 2008 at 08:59:28PM +0100, Andrew Coppin wrote:
>  let y = 5 in (f x) y
>
> ...and x is now a free variable. OOPS!
>
> Trying to tease out exactly under which conditions you can and cannot  
> perform the substitution is utterly maddening. Since this is a Haskell  
> mailing list and as such it is populated by vast numbers of people with  
> PhDs and so forth... does anybody happen to know the *correct* solution  
> to this conundrum? Before I become clinically insane...? o_O

A simple solution is to separate your 'substitution' and
'simplification' passes. As in, perform any substitutions you like, but
_keep_ the original binding for x.  let the simplifier/optimizer
recognize when bindings are dead and remove them. It can do so simply by
keeping track of free variables in the subterms, which is also useful
for things like let floating transformations.

        John

--

-- 
John Meacham - ⑆repetae.net⑆john⑈

headers

Lennart Augustsson | 27 Aug 23:25

Re: Compiler's bane

You can get rid of all recursive bindings by transforming them into a
use of a fixpoint combinator.
And then you can use a non-recursive definition of the fixpoint
combinator, and never worry about recursive bindings again.

  -- Lennart

On Wed, Aug 27, 2008 at 8:59 PM, Andrew Coppin
<andrewcoppin <at> btinternet.com> wrote:
> Hi guys.
>
> I'm writing a simple interpretter for a small extended-lambda-calculus sort
> of language. And I'd just like to say... RECURSIVE LET-BINDS! GAAAAH!!! >_<
>
> No other part of the program has consumed nearly as much brain power as me
> trying to figure out when it is and isn't safe to replace a variable with
> its RHS.
>
> To illustrate:
>
>  let x = f x; y = 5 in x y
>
> A simple-minded interpretter might try to replace every occurrance of "x"
> with "f x". This yields
>
>  let y = 5 in (f x) y
>
> ...and x is now a free variable. OOPS!
>
> Trying to tease out exactly under which conditions you can and cannot

(Continue reading)

headers

Jeremy Apthorp | 27 Aug 23:32

Re: Compiler's bane

2008/8/28 Lennart Augustsson <lennart <at> augustsson.net>:
> You can get rid of all recursive bindings by transforming them into a
> use of a fixpoint combinator.
> And then you can use a non-recursive definition of the fixpoint
> combinator, and never worry about recursive bindings again.

This[1] might be a good explanation of why that works. It helped me
understand it, at least.

[1] - http://mvanier.livejournal.com/2897.html

Jeremy