On Mon, Feb 16, 2015 at 2:22 AM, Keean Schupke <[email protected]> wrote: > I agree with most of what you have said over several posts. There are two > things I disagree with: > > - Type systems are logical frameworks, and keeping as close to some logic as > possible makes them most useful. In my own work I have included a Prolog > like logic interpreter in the type system so that simple types are inferred > (the inference algorithm is very short and elegant in logic too). Various > ad-hoc type system extensions can naturally be expressed in logic, and the > curry-howard isomorphism makes this an elegant approach. Logic and type - > systems really are the same thing.
Don't oversimplify. Yes, type systems and logics are the same, by Curry-Howard. But pragmatically, designing a type system for a programming language and designing a type system for proving theorems are not so simply related. And using Prolog for type inference is logic programming, not Curry-Howard. Maybe you knew that. > - That this necessarily means poor performance, or that you have to compile > like Haskell. My project uses unboxed types with no garbage collection and > compiled imperative code in the IO monad directly to 'C' like code. So > really performance is as 'C' but with a proper logical type system. Without going into details about your project, it's hard for me to tell whether you're being too optimistic about your project, or your project is a lot less like Haskell than you've been making it sound. You should pay attention to the problems Shap is talking about with curried pure functions, if your project is using them. > In all likelihood I am not going to persuade everyone that this is the right > approach for BitC, but I feel it is worth sharing the thoughts so far from > my own work and discussing, as I might learn something useful. That's the spirit! In all likelihood, you'll never convince Shap to use monadic effects, even if you could solve all his technical objections. That would be a huge stylistic change to BitC, which he probably thinks would alienate systems programmers. I've also failed to convince him to make a major stylistic change, and I'm still here. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
