Attempt at type checking in Datalog
omg type abstraction seems to work
*hokay* I fixed an actual bug.
HOKAY we have added real test cases which drastically simplify stuff.

heads

tip
browse log
simply-typed-lambda-calculus
browse .tar.gz

clone

read-only
https://hg.sr.ht/~icefox/pancake
read/write
ssh://hg@hg.sr.ht/~icefox/pancake

#Pancake

Noodling around with making a type checker using Datalog.

Started out as an exercise in learning datalog, but might actually be useful now. Uses the Rust crepe crate, which implements DL as a proc macro. Currently it just implements simply-typed lambda calculus.

Tried using Souffle: https://souffle-lang.github.io/program and its lack of a repl kinda irks, so this seems like the next best thing for me.