More sensibly, I imagine we could take a C program as is, and provide types for the terms. Expressions would be straightforward, statements a bit harder. To cope with 'value' semantics would require linear types. It may be you chose to avoid the stranger corners of C if you can.
We can write a 'C' emulator in pure lambda calculus, or perhaps better, compile 'C' to pure lambda calculus as a target. The types of these pure lambda terms would be the types of the C terms. You can then type check the 'C' terms, and then compile as normal with a 'C' compiler. Personally my interest is in merging a fast 'C' like language with a parametrically polymorphic type system. I am happy with imperative features being in the IO Monad. I am sort of considering 'C' to a more complex syntactic sugar over Haskell's 'do' notation. Keean. On 12 February 2015 at 16:51, 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 >> > >
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
