On 16 February 2015 at 08:37, Matt Oliveri <[email protected]> wrote:
> 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. > Actually they are both logics of varying soundness... > > And using Prolog for type inference is logic programming, not > Curry-Howard. Maybe you knew that. > Consider you infer a program type like: pair :: a -> b -> (a, b) This can be directly expressed in logic as: fun(pair, arrow(a, arrow(b, pair(a, b)))) Now consider type-classes like data Nil data Succ x = Succ x class Num x instance Num Nil instance (Num x) =>Num (Succ x) we can translate that into logic as: num(nil). num(succ(x)) :- num(x). Type classes are directly expressible in logic without the value level syntax (makes sense as we are computing at the type level). Values in the logic language are the types of the terms in the value language. Different logics result in different properties (for example linear logic == linear types) > > - 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. My thinking at the moment is that arities should be explicit in types, and that local arity-aliases would help solve the library style mismatch problem, without having to solve the general un-Currying problem. This seems a sensible approach, How to make the arity explicit is another question, various proposals have problems: a b c -> b c -> a Has the problem that the types look like polymorphic constructors, is: m a -> a a binary function, or a type with constructor polymorphism? (a, b, c) -> (b, c) -> a has the problem that we might try and pass a boxed tuple, which would be a single reference, not N separate values. Fn a b c -> Fn a b -> a a -> b -> c -> Fn (a -> b -> Fn a) have the problem that they look like a command and a monad respectively and I think an ML style function both depends on context and produces effects, so is actually an "Arrow" not a monad or a co-monad. This leaves the special-arrow syntax as being the most promising to me at this point in time: a -> b -> c => a -> b => a But this of course leaves the impression that curried application is still possible, which we don't want. So maybe the co-monad approach is the best after all? Fn a b c -> Fn a b -> a Viewing a function as a datatype, that you cannot create (sounds about right as we don't allow self-modifying code), that you can extract a value from. The co-monadic extract being function application. The more I think about this the more I like it, and it looks nice. Keean.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
