psilo

Hello! This is the incomplete source code for an unfinished programming language called psilo. There's a lot to say so I'm just writing this when I can; feel free to email me at gatlin+psilo@niltag.net.

Psilo aims to be:

• principled: contrast with "dogmatic," the language is motivated simply by good theory and bad experience;
• safe: the type system will be able to reason about context and behavior, and not merely traditional "square-peg-round-hole" verification;
• intuitive: an idea's implementation should emerge almost automatically from its description as a type, and best practices should reinforce legibility;
• linear: virtually everything in psilo emanates from Girard's Linear Logic;
• open: to new ideas, to all contributors and users, and also in a licensing sense.

What exists now

Currently psilo exists as a read-evaluate-print-loop (REPL) interpreter which evaluates expressions in an intermediate form of the language.

It lacks IO. There is no state. Every single program is a single closed expression.

But you can write, say, type-safe generators and folds:

‽> (letrec (
..   (yield (\ (value) (shift k (! (\ (p) ((? p) value k))))))
..   (next (\ (gen)
..     (let k ( (? gen) (! (\ (a b) b)))
..     (k _))))
..   (peek (\ (gen)
..     ( (? gen) (! (\ (a b) a)))))
..   )
.. (let gen (reset
..   (let _ ((? yield) 1)
..   (let _ ((? yield) 2)
..          ((? yield) 3))))
.. (let n1 ((? peek) gen)
.. (let gen ((? next) gen)
.. (let n2 ((? peek) gen)
.. (let gen ((? next) gen)
.. (let n3 ((? peek) gen)
.. (add-int n1 (add-int n2 n3))))))))
.. )
int
6

Or do recursion (with some non-linear control flow for fun):

‽> (letrec (
..   (seventeen (\ ()
..     (let r (reset
..       (let s (shift k
..         (let eight (k 4)
..         (k eight)))
..       (mul-int 2 s)))
..     (add-int r 1))))
..   (factorial (\ (n)
..     (letrec (
..       (helper (\ (n total)
..         (if (lt-int n 2)
..           total
..           ((? helper) (sub-int n 1) (mul-int n total) ))))
..     )
..     (let n (? n)
..     ((? helper) n 1) )
..     ) ))
.. )
.. ((? factorial) (! ((? seventeen)) ) )
.. )
int
355687428096000

And sure why not you can write this too:

‽> (letrec (
..   (foldr (λ (c e xs)
..     (let xs (? xs)
..     ( (? xs) c e ) )))
..
..   (nil (λ () (! (λ (c e) e))))
..
..   (cons (λ (x xs) (! (λ (c e)
..     ( (? c)
..         x
..         (! ( (? foldr)
..                c
..                e
..                xs )))))))
..
.. )
.. (let list-1
..   (! ((? cons) 1
..   (! ((? cons) 2
..   (! ((? nil)))))))
.. ( (? foldr)
..     (! (λ (a b)
..       (let a (? a)
..       (let b (? b)
..       (add-int a b)))))
..     7
..     list-1 ))
.. )
int
10

We like IO, mutable state, and sophisticated project management tools. But, the whole point is to do them in a particular way in concert with the type system.

You can review the language Syntax to learn a little about the syntax you're looking at. The evaluator, implemented as a CESKM machine, is written so that its implementation reads like the language's semantics. And, though it is as ambitious as it is incomplete, you can also check out the nascent Types module to read the (ongoing) type checking strategy.

Stay tuned!