This library provides both type level and runtime versions of a lazy functional language.
- static, all constants
- lazy, things only run if needed
- functional, all things are functions
- curryed, we can use partial application
SKI based, all other combinators are derivednot anymore, implemented many others as buitin code to obtain a more compact executable file- can fit into MCU's (specially the typelevel layer), hence the C++11 base.
cout<<toInt(length(list(1,2,3,4,"ok!")))<<endl;
cout<<toInt(foldl(mul)(n1)(list(n2,FromInt<120>{})))<<endl;
This pseudo-language uses C++11 compiler and works both at typelevel and runtime.
Functions have a duo, all function starting with a capital letter are compile time evaluated (type-level), others will work at runtime (compiled).
Head type level, result is a type or dependent type.
head runtime level, result is a value
Exploring functional paradigm
Extend C++ compiler
Use typelevel for small MCU's
implemented so far:
Flip - λfab.fba
used function f
with arguments in reverse order
Pair - λabf.fab
construct pair or values to deliver to function f
Fst - λo.o(λab.a)
get first element of a pair
Snd - λo.o(λab.b)
get second element of a pair
True - select first option λab.a
False - select second option λab.b
And - functional boolean and
Or - functional boolean or
Not - functional negation
BEq - boolean equality
using Church encoded numerals
Succ - successor of a nominal
Pred - predecessor or a nominal
N0 .. N9 - predefined numerals
Is0 - check if numeral is N0
Add - sum 2 numerals
Sub - subtract 2 numeral
Mul - multiply 2 numerals
Pow - numerals power
Eq - check numeral equality
NEq - check numeral inequality
LEq - check numeral <=
relation
GEq - check numeral >=
relation
Lt - check numeral <
relation
Gt - check numeral >
relation
Head - get first element of a list
Tail - get ramaining of a list (but the head)
Cons - construct a list node
Nil - empty list
Null - check if list is empty
Length - get list length (numeral)
Index - get element at index
Drop - drop elements from list head
Init - get list of all but last element
Last - get last element of a list
Reverse - reverse list order
Take - take elements from list start
Nats - list of all natural numbers (infinit list)
Range - range of integers (list)
Concat - join 2 lists
Map - map a function over list elements
Filter - filter list elements
FoldL - left fold a list with a function and start value
FoldR - right fold a list with a function and start value
Zip - join 2 lists in a list of pairs with minimal length
Nothing - λn.λj.n
Just - λxnj.j x
All above types have a runtime function with the same name but with a first low-case letter.
S:= - λfgo.f(g o)
K:= - λab.a
I:= - λo.o
B,C,M,L,Y,T,V,R,Bb,Id
toBool convert expression to c++ bool
toInt convert expression to c++ int (numeral to c++ int)
toStr convert expression to string or String, depending on the platform
print reduces and prints the expression reduction result.
now using c++ ostream for printing
list build a polymorphic list
example
List<StaticInt<1>,StaticText<&my_text>>;//compile time list build
List<int,const char*>{1,""};
list(1,2,"Ok");//runtime list built
https://www.angelfire.com/tx4/cus/combinator/birds.html
https://users.monash.edu/~lloyd/tildeFP/Lambda/Examples/const-list/
https://sincereflattery.blog/2021/04/26/lists-in-the-lambda-calculus/
https://blog.ploeh.dk/2018/06/04/church-encoded-maybe/
https://www.cl.cam.ac.uk/~rmk35/lambda_calculus/lambda_calculus.html