# 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:

**p**rincipled: contrast with "dogmatic," the language is motivated simply by good theory and bad experience;**s**afe: the type system will be able to reason about*context*and*behavior*, and not merely traditional "square-peg-round-hole" verification;**i**ntuitive: an idea's implementation should emerge almost automatically from its description as a type, and best practices should reinforce legibility;**l**inear: virtually everything in psilo emanates from Girard's Linear Logic;**o**pen: 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)))) .. (fact (\ (n) (letrec ( .. (help (\ (n total) .. (let n (? n) .. (let total (? total) .. (if (lt-int n 2) .. total .. ( (? help) (sub-int n 1) (mul-int n total) )))))) ) .. ( (? help) n 1)))) .. ) .. ((? fact) (! ((? 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!