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
