←back to thread

Show HN: Term-Lisp – A Lisp, based on pattern matching and term rewriting

(github.com)
58 points boris_m | 1 comments | 06 Nov 24 14:53 UTC | HN request time: 0.415s | source
Show context
BoiledCabbage ◴[06 Nov 24 18:07 UTC] No.42066515[source]▶
Term re-writing systems are a really interesting way of looking at computation.

It completely abstracts away the concept of a machine, and it's simply translation as computation - but equally as powerful.

replies(3): >>42066655 #>>42066678 #>>42067446 #
simplify ◴[06 Nov 24 18:16 UTC] No.42066655[source]▶
Agreed. This reminds me – and I wonder if it could be applied – to Computational Type Theory, which relies on a similar concept of "reducing" types to their primitive forms, actually taking computation into account (something type theories normally do not!)

This lecture series goes into how it works: https://www.youtube.com/watch?v=LE0SSLizYUI

replies(1): >>42072875 #
1. deterministic ◴[07 Nov 24 02:55 UTC] No.42072875[source]▶
I watched all 5 videos a few years ago. And if I understand it correctly "Computational Type Theory" basically defines a type as describing the behaviour of a computation.

Which is really interesting but kinda hard for me to wrap my arms around compared with Martin Loff type theory. It looks as if type checking will have to be done manual, using N axiomatic rules for how you can prove A from B.

Is that your understanding as well?

Also, there doesn't seem to be much material on Computational Type theory online. Any good references? (Except for the nuPrl book of course).