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 >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
