Lambda over types.

[anatoli]

--0-2060797451-1017916183=:35143
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline

(Redirected from haskell to haskell-cafe.)

Well, I tried to fix the problems you mention.
Results attached. I have managed to do without de Brujin 
notation. The evaluator is (modulo bugs!) normal order.
One can easily do an applicative order evaluator as well.
Evaluating to WHNF is probably easy too (this is what the 
previous version supposed to do).

I'll try to come up with a regression test suite for this
stuff as my (copious :) free time permits, but on the surface it
looks ok.

--- oleg@pobox.com wrote:
> 
> 
> anatoli <anatoli at yahoo> wrote:
> 
> > This is all, of course, of purely academical interest. The notation
> > is extremely inconvenient to do any real work. I'd rather prefer
> > a real, language-supported lambda over types.
> 
> > Or... wait a minute! You did find all those problems; does it mean
> > you tried to *use* this stuff for something? Just curious.
> 
> I must start with a profuse apology, because what follows is perhaps
> of little relevance to the list. I also propose to re-direct the
> follow-ups to the Haskell Cafe.
> 
> I have examined your code and then tried a few examples, some of which
> from my code's regression tests.
> 
> I have implemented a compile-time lambda-calculator, in a different
> language. I should say, in a meta-language. The output of the
> evaluator is a term that can then be compiled and evaluated. The
> lambda-calculator acts as a partial evaluator. The calculator
> normalizes a term in a pure untyped lambda calculus. The result is
> compiled and evaluated in a call-by-value lambda-calculus with
> constants.
> 
> Haskell typechecker (augmented with multi-parameter classes with
> functional dependencies and let on loose) may do something similar.
> 
> BTW, the meta-language lambda-evaluator code (with the regression tests)
> can be found at
> 	http://pobox.com/~oleg/ftp/Computation/rewriting-rule-lambda.txt
> The calculator is implemented in CPS, in some sort of extended lambda
> calculus. Therefore, the code has three kinds of lambdas: of the source
> language, of the transformer meta-language, and of the target
> language. The first and the third lambdas are spelled the same and
> are the same.
> 
> 
> _______________________________________________
> Haskell mailing list
> Haskell@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell



__________________________________________________
Do You Yahoo!?
Yahoo! Tax Center - online filing with TurboTax
http://taxes.yahoo.com/
--0-2060797451-1017916183=:35143
Content-Type: application/x-unknown; name="lambda.lhs"
Content-Transfer-Encoding: base64
Content-Description: lambda.lhs
Content-Disposition: attachment; filename="lambda.lhs"

PiBtb2R1bGUgTGFtYmRhIHdoZXJlCgpWYXJpYWJsZXMgCgo+IGRhdGEgWCA9
IFgKPiBkYXRhIE5leHQgYSA9IE5leHQgYQo+IHR5cGUgWDAgPSBYCj4gdHlw
ZSBYMSA9IE5leHQgWDAKPiB0eXBlIFgyID0gTmV4dCBYMQo+IHR5cGUgWDMg
PSBOZXh0IFgyCj4gdHlwZSBYNCA9IE5leHQgWDMKPiB0eXBlIFg1ID0gTmV4
dCBYNAo+IHR5cGUgWDYgPSBOZXh0IFg1Cgo+IHgwID0gWAo+IHgxID0gTmV4
dCB4MAo+IHgyID0gTmV4dCB4MQo+IHgzID0gTmV4dCB4Mgo+IHg0ID0gTmV4
dCB4Mwo+IHg1ID0gTmV4dCB4NAo+IHg2ID0gTmV4dCB4NQoKTGFtYmRhIGFi
c3RyYWN0aW9uIDogXHgtPnkKVXNlIFhpIGFzIHZhcmlhYmxlcy4KCj4gZGF0
YSBMIHggeSA9IEwgeCB5IHwgeCA6XCB5CgpBcHBsaWNhdGlvbiA6IHggeQoK
PiBkYXRhIEEgeCB5ID0gQSB4IHkgfCB4IDovIHkKCkdlbmVyYXRlIGZyZXNo
IHZhcmlhYmxlcyBmb3IgYWxwaGEtY29udmVyc2lvbi4KCj4gY2xhc3MgRnJl
c2hWYXIgYSBiIHwgYSAtPiBiIHdoZXJlCj4gICBmcmVzaFZhciA6OiBhIC0+
IGIKPiAgIGZyZXNoVmFyID0gdW5kZWZpbmVkCgo+IGluc3RhbmNlIEZyZXNo
VmFyIFggKE5leHQgWCkKPiBpbnN0YW5jZSBGcmVzaFZhciAoTmV4dCB4KSAo
TmV4dCAoTmV4dCB4KSkKCj4gY2xhc3MgTWF4VmFyIGEgYiBjIHwgYSBiIC0+
IGMgd2hlcmUKPiAgIG1heFZhciA6OiBhIC0+IGIgLT4gYwo+ICAgbWF4VmFy
ID0gdW5kZWZpbmVkCgo+IGluc3RhbmNlIE1heFZhciBYIFggWAo+IGluc3Rh
bmNlIE1heFZhciBYIChOZXh0IHgpIChOZXh0IHgpCj4gaW5zdGFuY2UgTWF4
VmFyIChOZXh0IHgpIFggKE5leHQgeCkKPiBpbnN0YW5jZSBNYXhWYXIgYSBi
IGMgPT4gTWF4VmFyIChOZXh0IGEpIChOZXh0IGIpIChOZXh0IGMpCgo+IGlu
c3RhbmNlIChGcmVzaFZhciB2IHgsIEZyZXNoVmFyIHQgeCcsIE1heFZhciB4
IHgnIHkpID0+IAo+ICAgICAgICAgIEZyZXNoVmFyIChMIHYgdCkgeQoKPiBp
bnN0YW5jZSAoRnJlc2hWYXIgdCB4LCBGcmVzaFZhciB0JyB4JywgTWF4VmFy
IHggeCcgeSkgPT4KPiAgICAgICAgICBGcmVzaFZhciAoQSB0IHQnKSB5CgpT
b21lIHV0aWxpdHkgY2xhc3NlcyBhbmQgdHlwZXMuCgo+IGRhdGEgVCA9IFQK
PiBkYXRhIEYgPSBGCgo+IGNsYXNzIE9yIHggeSB6IHwgeCB5IC0+IHoKPiBp
bnN0YW5jZSBPciBGIEYgRgo+IGluc3RhbmNlIE9yIFQgRiBUCj4gaW5zdGFu
Y2UgT3IgRiBUIFQKPiBpbnN0YW5jZSBPciBUIFQgVAoKPiBjbGFzcyBDaG9z
ZSB4IHkgeiB0IHwgeCB5IHogLT4gdAo+IGluc3RhbmNlIENob3NlIFQgeSB6
IHkKPiBpbnN0YW5jZSBDaG9zZSBGIHkgeiB6Cgo+IGNsYXNzIFNhbWVWYXIg
eCB5IHogfCB4IHkgLT4gego+IGluc3RhbmNlIFNhbWVWYXIgWCBYIFQKPiBp
bnN0YW5jZSBTYW1lVmFyIFggKE5leHQgeCkgRgo+IGluc3RhbmNlIFNhbWVW
YXIgKE5leHQgeCkgWCBGCj4gaW5zdGFuY2UgU2FtZVZhciB4IHkgeiA9PiBT
YW1lVmFyIChOZXh0IHgpIChOZXh0IHkpIHoKClRoaXMgd2lsbCBiZSB1c2Vm
dWwuLi4KCj4gaW5zdGFuY2UgU2FtZVZhciBYIChBIHggeSkgRgo+IGluc3Rh
bmNlIFNhbWVWYXIgKE5leHQgeCkgKEEgeCB5KSBGCj4gaW5zdGFuY2UgU2Ft
ZVZhciBYIChMIHggeSkgRgo+IGluc3RhbmNlIFNhbWVWYXIgKE5leHQgeCkg
KEwgeCB5KSBGCgo+IGNsYXNzIEZpcnN0T3JTZWNvbmRQbHVzIGEgYiBjIGQg
fCBhIGIgYyAtPiBkCj4gaW5zdGFuY2UgRmlyc3RPclNlY29uZFBsdXMgVCBi
IGMgYgo+IGluc3RhbmNlIEZpcnN0T3JTZWNvbmRQbHVzIEYgYiBjIChOZXh0
IGMpCgpTdWJzdGl0dXRpb25zLgoKPiBjbGFzcyBTdWJzdCB2YXIgZm9yVGVy
bSBpblRlcm0gcmVzdWx0IHRyeUFnYWluIHwKPiAgICAgICAgIHZhciBmb3JU
ZXJtIGluVGVybSAtPiByZXN1bHQgdHJ5QWdhaW4gd2hlcmUKPiAgIHN1YnN0
IDo6IHZhciAtPiBmb3JUZXJtIC0+IGluVGVybSAtPiAocmVzdWx0LCB0cnlB
Z2FpbikKPiAgIHN1YnN0ID0gdW5kZWZpbmVkCgpTdWJzdGl0dXRlIGEgdmFy
aWFibGUuCgo+IGluc3RhbmNlIFN1YnN0IFggZm9yVGVybSBYIGZvclRlcm0g
VAo+IGluc3RhbmNlIFN1YnN0IChOZXh0IHgpIGZvclRlcm0gWCBYIEYKPiBp
bnN0YW5jZSBTdWJzdCBYIGZvclRlcm0gKE5leHQgeCkgKE5leHQgeCkgRgo+
IGluc3RhbmNlIChTdWJzdCB4IGZvclRlcm0geSByZXN1bHQgdHJ5QWdhaW4s
Cj4gICAgICAgICAgIEZpcnN0T3JTZWNvbmRQbHVzIHRyeUFnYWluIHJlc3Vs
dCB5IHJlc3VsdCcpID0+Cj4gICAgICAgICAgU3Vic3QgKE5leHQgeCkgZm9y
VGVybSAoTmV4dCB5KSByZXN1bHQnIHRyeUFnYWluCgo+IGluc3RhbmNlIChT
dWJzdCB2YXIgZm9yVGVybSBpblRlcm0xIHJlc3VsdDEgdHJ5QWdhaW4xLAo+
ICAgICAgICAgICBTdWJzdCB2YXIgZm9yVGVybSBpblRlcm0yIHJlc3VsdDIg
dHJ5QWdhaW4yLAo+ICAgICAgICAgICBPciB0cnlBZ2FpbjEgdHJ5QWdhaW4y
IHRyeUFnYWluKSA9Pgo+ICAgICAgICAgIFN1YnN0IHZhciBmb3JUZXJtIChB
IGluVGVybTEgaW5UZXJtMikgKEEgcmVzdWx0MSByZXN1bHQyKSB0cnlBZ2Fp
bgoKVXRpbGl0eSBydWxlLgoKPiBjbGFzcyBTdWJzdElmTm90IGRvaXQgdmFy
IGZvclRlcm0gaW5UZXJtIHJlc3VsdCB0cnlBZ2FpbiB8Cj4gICAgICAgZG9p
dCB2YXIgZm9yVGVybSBpblRlcm0gLT4gcmVzdWx0IHRyeUFnYWluCj4gaW5z
dGFuY2UgU3Vic3RJZk5vdCBUIHZhciBmb3JUZXJtIGluVGVybSBpblRlcm0g
VAo+IGluc3RhbmNlIFN1YnN0IHZhciBmb3JUZXJtIGluVGVybSByZXN1bHQg
dHJ5QWdhaW4gPT4KPiAgICAgICAgICBTdWJzdElmTm90IEYgdmFyIGZvclRl
cm0gaW5UZXJtIHJlc3VsdCB0cnlBZ2FpbgoKT2khIEFscGhhLWNvbnZlcnNp
b24uCgo+IGluc3RhbmNlIChGcmVzaFZhciBmb3JUZXJtIGZyZXNoMSwKPiAg
ICAgICAgICAgRnJlc2hWYXIgaW5UZXJtIGZyZXNoMiwKPiAgICAgICAgICAg
RnJlc2hWYXIgdmFyJyBmcmVzaDMsCj4gICAgICAgICAgIE1heFZhciBmcmVz
aDEgZnJlc2gyIGZyZXNoNCwKPiAgICAgICAgICAgTWF4VmFyIGZyZXNoMyBm
cmVzaDQgbmV3RnJlc2gsCj4gICAgICAgICAgIFN1YnN0IHZhcicgbmV3RnJl
c2ggaW5UZXJtIHJlc3VsdCBpZ25vcmUsCj4gICAgICAgICAgIFN1YnN0IHZh
ciBmb3JUZXJtIHJlc3VsdCByZXN1bHQnIHRyeUFnYWluKSA9Pgo+ICAgICAg
ICAgIFN1YnN0IHZhciBmb3JUZXJtIChMIHZhcicgaW5UZXJtKSAoTCBuZXdG
cmVzaCByZXN1bHQnKSB0cnlBZ2FpbgoKTm93IGRvIHJlZHVjdGlvbnMuCgo+
IGNsYXNzIFJlZHVjZSBlIGUnIHRyeUFnYWluIHwgZSAtPiBlJyB0cnlBZ2Fp
biB3aGVyZQo+ICAgcmVkdWNlIDo6IGUgLT4gKGUnLCB0cnlBZ2FpbikKPiAg
IHJlZHVjZSA9IHVuZGVmaW5lZAoKUmVkdWNlIHZhcmlhYmxlIHRvIGl0c2Vs
Zi4KCj4gaW5zdGFuY2UgUmVkdWNlIFggWCBGCj4gaW5zdGFuY2UgUmVkdWNl
IChOZXh0IHgpIChOZXh0IHgpIEYKClJlZHVjZSBsYW1iZGEgYWJzdHJhY3Rp
b24uCgo+IGluc3RhbmNlIFJlZHVjZSB5IHknIHRyeUFnYWluID0+IFJlZHVj
ZSAoTCB4IHkpIChMIHggeScpIHRyeUFnYWluCgpBcHBsaWNhdGlvbi4KCj4g
Y2xhc3MgQXBwbHkgZnVuIGFyZyByZXN1bHQgdHJ5QWdhaW4gfCBmdW4gYXJn
IC0+IHJlc3VsdCB0cnlBZ2FpbgoKQXBwbHkgdmFyaWFibGUuCgo+IGluc3Rh
bmNlIChSZWR1Y2UgeSB5JyB0cnlBZ2FpbikgPT4gQXBwbHkgWCB5IChBIFgg
eScpIHRyeUFnYWluCgpBcHBseSBsYW1iZGEgYWJzdHJhY3Rpb24gOiBldGEg
b3IgYmV0YT8KCj4gaW5zdGFuY2UgKFNhbWVWYXIgeCBhcmcgc2FtZSwKPiAg
ICAgICAgICAgU3Vic3RJZk5vdCBzYW1lIHggYXJnIGZ1biByZXN1bHQgdHJ5
QWdhaW4sCj4gICAgICAgICAgIENob3NlIHNhbWUgZnVuIHJlc3VsdCByZXN1
bHQnKSA9Pgo+ICAgICAgICAgIEFwcGx5IChMIHggZnVuKSBhcmcgcmVzdWx0
JyB0cnlBZ2FpbgoKQW5vdGhlciB1dGlsaXR5IHJ1bGUuCgo+IGNsYXNzIFJl
ZHVjZUlmTm90IHRyeWl0IGUgZScgdHJ5QWdhaW4gfCB0cnlpdCBlIC0+IGUn
IHRyeUFnYWluCj4gaW5zdGFuY2UgUmVkdWNlSWZOb3QgVCBlIGUgRgo+IGlu
c3RhbmNlIFJlZHVjZSBlIGUnIHRyeUFnYWluID0+IFJlZHVjZUlmTm90IEYg
ZSBlJyB0cnlBZ2FpbgoKQXBwbHkgYXBwbGljYXRpb24uCgo+IGluc3RhbmNl
IChBcHBseSB4IHkgYXh5IHhUcnlBZ2FpbiwKPiAgICAgICAgICAgUmVkdWNl
SWZOb3QgeFRyeUFnYWluIHogcnogdHJ5QWdhaW4pID0+Cj4gICAgICAgICAg
QXBwbHkgKEEgeCB5KSB6IChBIGF4eSByeikgdHJ5QWdhaW4KClJlZHVjZSBh
cHBsaWNhdGlvbi4KCj4gaW5zdGFuY2UgQXBwbHkgeCB5IHJlc3VsdCB0cnlB
Z2FpbiA9Pgo+ICAgICAgICAgIFJlZHVjZSAoQSB4IHkpIHJlc3VsdCB0cnlB
Z2FpbgoKTG9vcCEKCj4gY2xhc3MgUmVkdWNlTG9vcCBsb29wIGUgZScgfCBs
b29wIGUgLT4gZScKClRoaXMgaW5zdGFuY2UgaXMgdW5kZWNpZGFibGUhCgo+
IGluc3RhbmNlIFJlZHVjZUxvb3AgRiBlIGUKPiBpbnN0YW5jZSAoUmVkdWNl
IGUgZScgdHJ5QWdhaW4sCj4gICAgICAgICAgIFJlZHVjZUxvb3AgdHJ5QWdh
aW4gZScgZScnKSA9PiAKPiAgICAgICAgICBSZWR1Y2VMb29wIFQgZSBlJycK
Cj4gY2xhc3MgRXZhbCBlIGUnIHwgZSAtPiBlJyB3aGVyZQo+ICAgZXZhbCA6
OiBlIC0+IGUnCj4gICBldmFsID0gdW5kZWZpbmVkCgpUaGlzIG9uZSBpcyBm
bGFnZ2VkIGFzIHVuZGVjaWRhYmxlIGFzIHdlbGwuCgo+IGluc3RhbmNlIFJl
ZHVjZUxvb3AgVCBlIGUnID0+IEV2YWwgZSBlJwoKRXhhbXBsZTogZXZhbHVh
dGUgcGFpcnMuCgo+IGluc3RhbmNlIChTdWJzdCB2YXIgZm9yVGVybSBhIGEn
IGFUcnlBZ2FpbiwKPiAgICAgICAgICAgU3Vic3QgdmFyIGZvclRlcm0gYiBi
JyBiVHJ5QWdhaW4nLAo+ICAgICAgICAgICBPciBhVHJ5QWdhaW4gYlRyeUFn
YWluJyB0cnlBZ2FpbikgPT4KPiAgICAgICAgICBTdWJzdCB2YXIgZm9yVGVy
bSAoYSxiKSAoYScsIGInKSB0cnlBZ2FpbgoKPiBpbnN0YW5jZSAoUmVkdWNl
IGEgYScgYVRyeUFnYWluLAo+ICAgICAgICAgICBSZWR1Y2VJZk5vdCBhVHJ5
QWdhaW4gYiBiJyB0cnlBZ2FpbikgPT4KPiAgICAgICAgICBSZWR1Y2UgKGEs
YikgKGEnLGInKSB0cnlBZ2Fpbgo=

--0-2060797451-1017916183=:35143--