I’m admitting that continuing making the c(x) language has grown into a full-blown side project again in past months, after a 10 year break… This post can be seen as a short tour into what the current implementation is capable of, but more precisely - how Effects work here, with a bunch of working examples!
TLDR
getOdd : Int -> Option Int // implementation omitted
checkPositive : Int -> Throw Int // implementation omitted
program : Int -> (MyIO || Throw || Option) Int
program number =
y <- read Int
x <- getOdd number
z <- checkPositive y
return (x + z)
myIOHandler = MyIO
& has read = ... // custom read impl
a <- read Int
b <- myIOHandler (program a)
print (show result)
// 1 1 -> ok 2
// 2 1 -> none
// 0 0 -> none
// 1 9 -> exception "fail"
Intro
Shortly, it’s a language where you can write typelevel code with the same language as usual runtime code. Functions are unified with types, and runtime values can be dependencies for types as well, even though it’s statically typed and compiled. Previously I’ve been referring to it as a gradually typed language, but now I don’t think so: constraints and proofs can be established by minimal checks on runtime input. Once a constraint is established, the compiler can use to erase all type logic.
do-notation from Haskell is a very powerful thing capable of encoding any logic behind a sequence of operations. It even can be READABLE (when you don’t write too crazy stuff with it). Here is an example usage of throw semantics implemented in terms of the language using monads:
program : Int -> Throw Int
program x =
if x < 0
throw "error! it's negative"
if x > 100
throw "error! it's too big"
return 12
// but there is no `do` keyword in `c(x)` - multiline blocks are
// automatically turned into sequences of `bind` when they're
// in monadic context.
try program
(exception s -> print s
exit)
Pure monads usually can’t be combined too easily (e.g. Throw with some other monad at the same time) - it’s order dependent and requires monads adapting to each other. You can’t write both in the same do block. I don’t fully like monad transformers, effects, polysemy, fused-effects, etc, and lifting anything other than weights. There is so much boilerplate, and the code is absolutely not readable for people not familiar with how that works - it turns into math.
Algebraic effects are closely related and in some implementations possess the same problem - combining them sometimes is not easy. Some implementations make it easier using hidden machinery. c(x), it seems, can be very minimalistic about it and shapes that the language supports allow you to define a construct that looks and behaves like effects - I find it pretty.
I’ll get to effects themselves in the end. Let’s see how I think monads can be combined and how it works so far in c(x).
Combining Monads - Demonstration
I came up with a simple solution that uses intersections and unions (those two conveniently happen to be c(x)’s fundamental operations), and I’m testing it for a few weeks. Here we go:
getOdd : Int -> Option Int // implementation omitted
checkPositive : Int -> Throw Int // implementation omitted
program : Int -> (Throw || Option) Int
program number = x <- getOdd number
y <- checkPositive x
return (y + 1)
// 5 -> ok 6
// 4 -> none
// 0 -> none
// -1 -> exception "fail"
Now let’s see what’s going on.
Or Else
So there is this || (“or else”) operation in the language. Simplified: intersecting a value with A || B tries to intersect with A, and if it’s an empty set, it tries to intersect with B. Then the system returns the intersected result. Pattern matching is expressed via that exact operation:
f 0 = 1
x = 42
print (show (f 0)) // output: 1
print (show (f 1)) // output: 42
// an equivalent definition:
f = (0 -> 1) || (x -> 42)
This operation works the same way if we expand it to type-level functions.
Has
Let’s get to another area. Regular function definitions don’t allow extending the domain this way:
f 0 = 0
f 1 = 1 // error! Intersection of (0 -> 0) and (1 -> 1) is empty
So called has-fields are just extensible functions/mappings. This is the only difference, besides syntax.
The smallest example is a simple record:
Person = has name : String
person : Person
& has name = "Ada"
print (name person) // output: Ada
So, the name is “keyed” on the object person.
Interface and Implementation
Fields can be combined and intersected. This shape allows us to make an interface and an implementation.
// interface
Greeting = has greet : String -> String
friendly : Greeting
& has greet who = "hi, " + who
// usage
runGreeting : Greeting -> String
runGreeting greeting = greeting:greet "Ada"
print (runGreeting friendly) // output: hi, Ada
Greeting states the requirement, and the second constraint supplies the implementation on friendly. & requires both to hold. It does not mean that the later definition overwrites the earlier one: incompatible constraints reject.
Generics
for is not a loop. It’s universal quantification (and it can take shape of loop).
Here is a generic identity function with a type annotation that says that the input and output types have to be the same.
identity : for a
a -> a
identity x = x
Methods can be generic too, parameterized on the argument to the datatype or not.
MyType t = has myMethod : for a
a -> t -> a
Typeclass
This is a construct from functional languages, meaning that the types that are instances of the typeclass support some operation. Say, integers are Addable because they support +. Or they are Monoid because they have some kind of addition and a zero element.
// typeclass
Monoid t = has zero : t
add : t -> t -> t
// instance
Int : Monoid Int
& has zero = 0
add = (+)
print (show (add Int 2 3)) // output: 5
But using it like this is not the best. add defined like above has to take the Int itself first, like add Int 1 2 = 3. I ain’t writing it that way! It is possible to make it pick up the type implicitly. This is currently done using weird type machinery. Soon I will probably make a syntactic sugar for it, but this is how it would be defined now within a library:
Monoid t = has zeroOf : t
addOf : t -> t -> t
add : for a (a -> a -> a)
add (a x) y = addOf a x y
zero : for a (a & {zeroOf a})
Then, to make it an instance, you can just:
Int : Monoid Int
& has zeroOf = 0
addOf = (+)
// usage
print (show (add 2 3)) // output: 5
A Sudden Monad Tutorial
Monads are also a typeclass with two operations - return and bind (there are some more requirements, but they are omitted for simplicity now). Let’s see what they are used for. We have an “optional” type, none OR some.
Option t = {some (x: t) | none}
And we want to use it that way:
program : Option Int
program =
a <- some 2
b <- myOperation a // might return "none", then the whole program returns "none"
c <- myOperation2 b
return (b + c) // otherwise returns "some (b + c)"
Let’s see what’s behind. These methods make that <- work. They are picked up by language machinery by name:
return : for [f : Monad, a]
a -> f a
bind : for [f : Monad, a, b]
f a -> (a -> f b) -> f b
returnwraps the value into the context.bindtakes a value in the context, then takes a continuation that takes a value without the context, returns a new value in the context, and then merges two layers of context and returns it in a new value.
Option t : has returnOf : for a
a -> Option a
returnOf v = some v
bindOf : for [a, b]
Option a -> (a -> Option b) -> Option b
bindOf (some x) g = g x
none g = none
And that’s it!
checkIfPositive (x: Int) = if x > 0
some x
else
none
program : Int -> Int -> Int -> Option Int
program (x: Int) (y: Int) (z: Int) =
a <- checkIfPositive x
b <- checkIfPositive y
c <- checkIfPositive z
return (a + b + c)
Combining has-methods
The coolest thing is that has-methods can be combined!
Intersection:
MyType1 = has f : Int -> Int
MyType2 = has g : Int -> Int
x : MyType1 & MyType2 // x is an object that has both
Intersecting same method = interface and implementation
MyType1 = has f : Int -> Int
MyType2 = has f : Int -> Int = (+1)
x : MyType1 & MyType2 // x has narrower definition from MyType2!
// incompatible definitions would error out
It works with or-else too. It can be used to create overloading:
MyType1 = has f (n : Int) = n + 1
MyType2 = has f (n : Float) = n + 1.0
x : MyType1 || MyType2
print (show (x:f 1)) // output: 2
print (show (x:f 1.0)) // output: 2.0
Now the remaining case is this:
MyType1 = has f : Int -> Int
MyType2 = has g : Int -> Int
x : MyType1 || MyType2
This is not useful in such simple case, but it comes in handy when combining monads!
Combining ordinary monads
Let’s use two small monads:
Option A = {some (value: A) | none}
Throw A = {ok (value: A) | exception (message: String)}
Two example functions in each. We will omit Monad definitions - we seen it above.
getOdd : Int -> Option Int
getOdd number =
if number % 2 = 0
none
else
some number
checkPositive : Int -> Throw Int
checkPositive number =
if number > 0
ok number
else
exception "fail"
Now let’s combine contexts!!!
This example needs bindOf implementations whose result types remain open to the
other context. The earlier Option signature explicitly returns Option b and
therefore cannot compose with a Throw continuation. Use open-result
implementations for this separate example:
Option A : has bindOf (some value) next = next value
none next = none
Throw A : has bindOf (ok value) next = next value
(exception message) next = exception message
program : Int -> (Throw || Option) Int
program number =
x <- getOdd number
y <- checkPositive x
returnOf (Throw || Option) (y + 1)
Each explicit <- selects the applicable bindOf. The final returnOf call
selects completion explicitly for the declared result context.
But I didn’t mention something…
Usual Bind Doesn’t Work. Polymonads?
It’s type is f a → (a → f b) → f b. It doesn’t match sequencing our functions - they are in one monad, but for our case we would need to have return value to be different! Something else that bind is required for composition.
A generalized bind can have the form:
f1 a -> (a -> f2 b) -> f3 b
That is the shape studied by polymonads, with additional laws governing composition. While it is not mathematically proven that c(x) uses polymonad, one can see that generalized bind here is a bit narrower: f2 needs to have a non empty intersection with f1 and f3.
So, in c(x) we still have usual bind for monads. The <- operator uses it, but the machinery behind it is a bit more complex. Formalizing it now is not a priority.
Return Value
This idea works for a trivial case. Two monad instances are tied to two datatypes with their own alternatives. First example at the top of the page is just a union of 4 variants.
But what if they overlap? What if you need to do something in the second monad every time something specific happens in the first monad? This is not a trivial case. Luckily, this is easily overridable by creating a new handler and you can achieve maximum flexibility this way too.
Effects
Effects are another powerful abstraction, similar to monads (effects can be implemented via monads OR concrete monads might be seen as implementations of concrete effects). You can define a set of “effectful computations” which later can be implemented by handlers. You can have programs made of these abstract operations (free monad). The effects themselves are interfaces for some system of operations. For example, whole IO can be abstracted away, and you can run the same code in a testing context that reads and prints in the way you need.
An operation can have a declared contract while leaving its implementation for an outside handler to supply. The program uses a public function, and the public function selects a member from its inferred, locally refined receiver.
Throw A = {completed (value: A) | exception (message: String)}
Throw A : has
returnOf value = completed value
bindOf (completed value) next = next value
(exception message) next = exception message
throwOf : String -> Throw A
throw = ... // omitted for simplicity
program : String -> Throw Int
program message =
n <- throw message
return (n + 1)
Now we have an effect interface Throw and an abstract program that doesn’t specify what exactly throw does. Let’s provide some implementations!
exceptionHandler = Throw Int
& has throwOf message = exception message
prefixedHandler = Throw Int
& has throwOf message = exception ("other: " + message)
print (show (exceptionHandler (program "boom"))) // output: exception "boom"
print (show (prefixedHandler (program "boom"))) // output: exception "other: boom"
One special c(x) core mechanic allows these handlers to be applied from outside - you could choose them on runtime! I’ll tell about it in the next article, but here is it in action:
exceptionHandler = Throw Int
& has throwOf message = exception message
prefixedHandler = Throw Int
& has throwOf message = exception ("other: " + message)
print (show (exceptionHandler (program "boom"))) // output: exception "boom"
print (show (prefixedHandler (program "boom"))) // output: exception "other: boom"
// shortest inline form!
print (show ((has throwOf = exception) (program "boom")))
The handler declaration constrains one subject to have both the Throw Int datatype constraint and the supplied method. This uses the same general member refinement as above examples.
Similarly, Throw could have abstract bindOf and the user would be able to introduce different behavior for it, e.g. logging errors and continuing.
Applying exceptionHandler refines the function/computation type for that application. The refinement propagates to its unresolved operation receiver, so throwOf (f a) sees the locally supplied implementation.
Outro
There still might be some rough edges, and I’m testing which combinations behave the way I expect - the most important parts were vibe-proofed with Lean. I’d love to hear your criticisms!
The syntax for effects is very minimal, as I want the same operations to work both on type and value level, so on surface, everything works using has-methods, set intersections, and “partial identity” functions/predicates, which I’ll tell about in the next post.