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     ┊   ╚════════════════════════════════╝