I do not consider TAL to be an instance of the bad idea with lambda calculus models that I outlined. Anyway, I thought TAL was designed as a target for certifying compilers for functional languages, so it's probably not good for something like BitC either.
Actually I know it's not good for BitC, because it doesn't support all the typing tricks that BitC would need. But I don't think it could be extended to something appropriate for BitC either. On Thu, Feb 12, 2015 at 11:51 AM, Keean Schupke <[email protected]> wrote: > I am looking at TAL (typed assembly language) as an interesting project in > this regard. If you can type assembly language, you can type 'C', which is > basically a cross-platform assembly language :-) > > Keean. > > > On 12 February 2015 at 16:43, Matt Oliveri <[email protected]> wrote: >> >> On Thu, Feb 12, 2015 at 11:12 AM, Keean Schupke <[email protected]> wrote: >> > >> > On 12 Feb 2015 16:02, "Jonathan S. Shapiro" <[email protected]> wrote: >> >> >> >> On Thu, Feb 12, 2015 at 2:06 AM, Keean Schupke <[email protected]> >> >> wrote: >> >>> >> >>> To expand on my last point, I think a pure lambda calculus can model >> >>> any >> >>> computation. I think a type system restricts the admissable lambda >> >>> terms to >> >>> a subset with your desired semantics. I think you can then directly >> >>> compile >> >>> that semantics. >> >>> >> >>> For example starting from a pure lambda calculus you can have a type >> >>> system that admits terms with the same semantics as C... >> >> >> >> This is an excellent summary of the "pure type theorist's" view of >> >> things. >> >> It is correct only because the pure type theory view does not consider >> >> computational performance (latency) to be part of semantics. In this >> >> view, a >> >> program that takes 100,000x as long to run as it should is perfectly >> >> acceptable, because it models the computation. >> >> >> >> The user who dies still waiting for that answer may have a different >> >> opinion. >> >>> >> >>> You can then compile this directly to assembly in the same way a C >> >>> compiler does. >> >> >> >> No. You can't. Because your definition of semantics excludes essential >> >> information that the C compiler requires in order to produce the >> >> assembly >> >> code that it produces. >> > >> > I disagree, and because my own project depends on this, I would be >> > interested to understand your reasons for thinking this. >> >> I think Keean is technically right that a model in pure lambda >> calculus could compile down to something sensible, given the right >> type system. But in order to do that, you'd practically have to say >> everything you'd say in a more sensible language, but indirectly. >> >> For example, lambda calculus has Church nats, which are HOFs, and HOFs >> aren't anywhere near as fast as machine words. But with the right >> type: "this HOF is a Church nat less than 2^64", the compiler could >> say "ah I see, screw HOFs." >> >> But in that example, it would've been easier just to have uint64. So >> you could technically turn any sensible language into a contrived pure >> lambda calculus model + type system that can generate the same code. >> But you've accomplished nothing. You have the same design problems, >> they're just now more verbose, and deal with lambda terms which aren't >> buying you anything. >> >> So I don't know if that's what Keean means, but that's how he could >> technically be right AFAIK. But anyway, it isn't solving any problems, >> it's just pushing them somewhere else. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
