3 ms·

Linear Logic, Linear Lisp, Linear Types and Concatenative Languages: https://cdiggins.github.io/blog/linear-logic-and-linear-lisp.html https://cdiggins.github.i

Linear Logic, Linear Lisp, Linear Types and Concatenative Languages: https://cdiggins.github.io/blog/linear-logic-and-linear-lisp.html https://cdiggins.github.io/blog/linear-logic-and-linear-lisp...

carapace 7y ago
Oh awesome. See also Conal Elliott's "Compiling to categories" ( http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/ ) where he is converting Haskell automatically to point-free form (like a concatinative language but not quite) and then instantiating that over different Categories to get different correct programs from the same expression. I've been working with Joy recently and I think this stuff is "the next big thing" for PLs. http://joypy.osdn.io/notebooks/Types.html http://joypy.osdn.io/notebooks/Types.html
- bjourne 7y ago
  Cool project! I've been working on typing for stack-based languages. Although I got stuck trying to make the inferencer work on higher-order functions. Kleffner's Master thesis supposedly explains how to accomplish that, but I haven't been able to wrap my head around it yet. I'd be interested to hear how you have solved the problem in Thun.
  - carapace 7y ago
    My original implementation is in Python and I documented a bit of research and implementation of type inference here: "The Blissful Elegance of Typing Joy" http://joypy.osdn.io/notebooks/Types.html http://joypy.osdn.io/notebooks/Types.html The “Type Inference in Stack-Based Programming Languages” talk given by Rob Kleffner informed it. I don't recall now whether I read his thesis but it's likely. I probably couldn't wrap my head around it either. For typing combinators (Joy's higher-order functions) I tried making a hybrid inferencer and interpreter that just evaluated them and it worked. (Incidentally that's what drove home to me the categorical nature of Joy. When I read Conal Elliott's "Compiling to Categories" I recognized what I had done.) In Joy the higher order combinators "don't care" if they are working on e.g. values or types. In other words they only care about the shape or structure (structural typing) of the data on the stack. When I wrote the interpreter in Prolog and then wrote the inferencer in Prolog I noticed they were the same code, so I deleted one of them. In Prolog, you can pass a stack and compute values or pass logic variables and it will tell you what kind of stack a given expression expects/generates. If you implement math ops with CLP(FD) you get a nice constraint compiler that get generate new Prolog implementations of Joy expressions. Sick, eh? In both Prolog and Python I haven't yet closed the loop for recursive combinators. Meaning the type inferencer generates the base-case and then the case for recurring once, then twice, and so on. I know the answer is some simple application of fixed-point theory or something, but I'm an idiot, and I've been working on other aspects (because I'm sure the solution is like decades old in the "compiling FP languages" literature. "Somebody else has had this problem.") In any event, I don't think I'll have to figure it out, because I just found out that the next steps I was going to take have already been done by the "Seven Sketches" folks and then some: https://news.ycombinator.com/item?id=20376325 https://news.ycombinator.com/item?id=20376325 I'm pretty sure most of that stuff would make great Joy combinators. And something in there would be the way to deal with e.g. genrec and x combinators.

Linear Logic, Linear Lisp, Linear Types and Concatenative Languages: https://cdiggins.github.io/blog/linear-logic-and-linear-lisp.html https://cdiggins.github.io/blog/linear-logic-and-linear-lisp...

carapace 7y ago

Oh awesome. See also Conal Elliott's "Compiling to categories" ( http://conal.net/papers/compiling-to-categories/ http://conal.net/papers/compiling-to-categories/ ) where he is converting Haskell automatically to point-free form (like a concatinative language but not quite) and then instantiating that over different Categories to get different correct programs from the same expression. I've been working with Joy recently and I think this stuff is "the next big thing" for PLs. http://joypy.osdn.io/notebooks/Types.html http://joypy.osdn.io/notebooks/Types.html

bjourne 7y ago
Cool project! I've been working on typing for stack-based languages. Although I got stuck trying to make the inferencer work on higher-order functions. Kleffner's Master thesis supposedly explains how to accomplish that, but I haven't been able to wrap my head around it yet. I'd be interested to hear how you have solved the problem in Thun.
- carapace 7y ago
  My original implementation is in Python and I documented a bit of research and implementation of type inference here: "The Blissful Elegance of Typing Joy" http://joypy.osdn.io/notebooks/Types.html http://joypy.osdn.io/notebooks/Types.html The “Type Inference in Stack-Based Programming Languages” talk given by Rob Kleffner informed it. I don't recall now whether I read his thesis but it's likely. I probably couldn't wrap my head around it either. For typing combinators (Joy's higher-order functions) I tried making a hybrid inferencer and interpreter that just evaluated them and it worked. (Incidentally that's what drove home to me the categorical nature of Joy. When I read Conal Elliott's "Compiling to Categories" I recognized what I had done.) In Joy the higher order combinators "don't care" if they are working on e.g. values or types. In other words they only care about the shape or structure (structural typing) of the data on the stack. When I wrote the interpreter in Prolog and then wrote the inferencer in Prolog I noticed they were the same code, so I deleted one of them. In Prolog, you can pass a stack and compute values or pass logic variables and it will tell you what kind of stack a given expression expects/generates. If you implement math ops with CLP(FD) you get a nice constraint compiler that get generate new Prolog implementations of Joy expressions. Sick, eh? In both Prolog and Python I haven't yet closed the loop for recursive combinators. Meaning the type inferencer generates the base-case and then the case for recurring once, then twice, and so on. I know the answer is some simple application of fixed-point theory or something, but I'm an idiot, and I've been working on other aspects (because I'm sure the solution is like decades old in the "compiling FP languages" literature. "Somebody else has had this problem.") In any event, I don't think I'll have to figure it out, because I just found out that the next steps I was going to take have already been done by the "Seven Sketches" folks and then some: https://news.ycombinator.com/item?id=20376325 https://news.ycombinator.com/item?id=20376325 I'm pretty sure most of that stuff would make great Joy combinators. And something in there would be the way to deal with e.g. genrec and x combinators.