Introduction

Solera is a small pure functional programming language. Its basic features:

HM + typeclasses
Algebraic data types
Tagless-final effects (planned)
Comptime (planned)
Mixfix operators (planned)

This basis is intended to be comfortable for the large majority of programmers familiar with the functional paradigm, whether coming from Rust, Haskell, Agda, Lean, etc. These features compose into a highly capable system, useful for hosting guest type systems as libraries within the language.

Comptime DSLs

Novel type systems are DSLs, built with ADTs and tagless-final, they are run at comptime allowing typechecking.

The resulting program is type-safe in both the Solera type system, and the guest type system.

 time --->                     COMPILE TIME ┊ RUNTIME
════════════════════════════════════════════╪════════════════════════════════════════
 Solera language                            ┊
 Guest type system as library               ┊
  |                    Guest language       ┊
  |                     |                   ┊
  V           (pass)    V          (pass)   ┊
 Solera type --------> Guest type --------> ┊ Run Solera code ---> Guest interpreter
 checker               checker              ┊                      (if any)
  |                     |                   ┊
  | (fail)              | (fail)            ┊   ╔════════════════════════════════╗
  V                     V                   ┊   ║ type-safe in BOTH type systems ║
 Solera type error     Guest type error     ┊   ╚════════════════════════════════╝

Getting started

First, clone the repo.

In the repo:

cabal run solera -- repl

> let id = \x -> x in id 7
7 : Int
> letrec fac = \n -> if (eq n 0) 1 (mul n (fac (sub n 1))) in fac 5
120 : Int

Roadmap

Planned syntax

Hello world

main : Out c => c ()
main = print "Hello world"

Top-level defs

-- Optional type annotations.
id x = x

const : a -> b -> a
const x y = x

ADTs

Point a = @data {
  x : a,
  y : a
}

List a = @data Cons a (List a)
             | Nil

-- Optional kind annotations.
Functor : * -> *
Functor f = @class
  { map : (a -> b) -> f a -> f b
  , _<*_ : a -> f b -> f a
  }

Comptime

-- The List example from before can be rewritten as:
List a = @data
  { Cons a $ List a
  | Nil
  }

-- At comptime, everything is values.
-- Here, $ treats types as values,
-- so the compiler infers it must be comptime.

Keyboard shortcuts

Solera