A simple modular extendible statically-typed symbolic programming language with dependent types. Implemented in Haskell.
simple:
- clean and simple "low-level" functional programming language
- explicit abstract syntax i.e. parentheses are required
- inspired Gallina and the ML family (but without many extras)
- no annoying "syntactical-sugar" constructions built-in; all syntax is consistent and modular
extendible:
- interface for easy implementations of macros and language constructs into pre-processor
- inspired by Racket and Coq's
Notation
modular:
- straighforward module system
- doesn't depend of file structure i.e. compilation/interpretation is done after concatenating all sourcecode together
statically-typed:
- complete compile-time type-checking enforcement
- (named) typed holes in the form of
Assumptions
symbolic:
- symbolic representations of values
- if
fis not defined and(f x)is evaluated,fis assumed to have the correct type and the value is the symbolic expression(f x) - if two functions
fandgare assumed this way and then compared (e.g.f x = g xis written) they are treated as distinct since their names are distinct
dependent types:
- type constructors e.g.
list : type -> type - value-dependent types e.g.
finite : nat -> type - type variables e.g.
mul_identity : forall n:nat, n * 1 = n - explicit polymorphism e.g.
empty_list : forall a:type, list a - infinite type hierarchy e.g.
(type = type0) : type1 : type2 : type3 : ...
| directory | description |
|---|---|
src/ |
haskell source-code. |
app/ |
haskell executable source-code. |
test/ |
haskell unit tests. |
doc/ |
haskell documentation. |
design/ |
reader-friendly design details (LaTex/PDF) |
examples/ |
example functive prorams. |
Using stack.
stack buildRun unit tests with
stack testRun executable (app/Main.hs) with
stack exec functive-hs-exeTODO