Last active
February 23, 2024 06:37
-
-
Save forked-from-1kasper/7bccc1e4b2aaaf6e559b97b06717572f to your computer and use it in GitHub Desktop.
Dependent Type Theory on Bash
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #! /usr/bin/bash | |
| # $ echo -n Π U Z Π 0 Π 1 U Z > Id | |
| # $ ./dtt.sh λ U Z λ 0 λ 1 β β β Id 2 1 0 | |
| # INFER: Π U Z Π 0 Π 1 U Z | |
| # EVAL: λ U Z λ 0 λ 1 β β β Id 2 1 0 | |
| function head() { | |
| echo $* | cut -d" " -f1 | |
| } | |
| function tail() { | |
| echo $* | cut -s -d" " -f2- | |
| } | |
| retval="" | |
| stack="" | |
| function pop() { | |
| local value=$(head "$stack") | |
| stack=$(tail "$stack") | |
| retval=$value | |
| } | |
| function push() { | |
| stack="$* $stack" | |
| } | |
| function dup() { | |
| pop | |
| push "$retval" | |
| push "$retval" | |
| } | |
| function term() { | |
| pop | |
| local leading="$retval" | |
| if [ "$leading" = "U" ]; then | |
| term | |
| local level="$retval" | |
| retval="U $level" | |
| return | |
| fi | |
| if [ "$leading" = "Π" ] || [ "$leading" = "λ" ] || [ "$leading" = "β" ]; then | |
| term | |
| local arg1="$retval" | |
| term | |
| local arg2="$retval" | |
| retval="$leading $arg1 $arg2" | |
| return | |
| fi | |
| retval="$leading" | |
| } | |
| # Evaluator | |
| function shift() { | |
| local i=$1 | |
| local c=$2 | |
| pop | |
| local leading="$retval" | |
| if [ "$leading" = "U" ]; then | |
| pop | |
| local level="$retval" | |
| retval="U $level" | |
| return | |
| fi | |
| if [ "$leading" = "Π" ] || [ "$leading" = "λ" ]; then | |
| shift $i $c | |
| local type="$retval" | |
| shift $i $((c+1)) | |
| local clos="$retval" | |
| retval="$leading $type $clos" | |
| return | |
| fi | |
| if [ "$leading" = "β" ]; then | |
| shift $i $c | |
| local fun="$retval" | |
| shift $i $c | |
| local arg="$retval" | |
| retval="β $fun $arg" | |
| return | |
| fi | |
| case $leading in | |
| ''|*[!0-9]*) retval="$leading" ;; | |
| *) | |
| if [ "$leading" -lt "$c" ]; then | |
| retval="$leading" | |
| else | |
| retval=$((leading+i)) | |
| fi | |
| esac | |
| } | |
| function up() { | |
| shift 1 0 | |
| } | |
| function down() { | |
| shift -1 0 | |
| } | |
| function app() { | |
| pop | |
| local leading="$retval" | |
| if [ "$leading" = "λ" ]; then | |
| term # unused type information | |
| term | |
| local clos="$retval" | |
| term | |
| push "$retval" | |
| up | |
| local arg="$retval" | |
| push "$clos" | |
| subst 0 "$arg" | |
| push "$retval" | |
| down | |
| return | |
| fi | |
| push "$leading" | |
| term | |
| local arg1="$retval" | |
| term | |
| local arg2="$retval" | |
| retval="β $arg1 $arg2" | |
| } | |
| function subst() { | |
| local i=$1 | |
| local t="$2" | |
| pop | |
| local leading="$retval" | |
| if [ "$leading" = "U" ]; then | |
| pop | |
| local level="$retval" | |
| retval="U $level" | |
| return | |
| fi | |
| if [ "$leading" = "Π" ] || [ "$leading" = "λ" ]; then | |
| subst $i "$t" | |
| local type="$retval" | |
| push "$t" | |
| up | |
| subst $((i+1)) "$retval" | |
| local clos="$retval" | |
| retval="$leading $type $clos" | |
| return | |
| fi | |
| if [ "$leading" = "β" ]; then | |
| subst $i "$t" | |
| local fun="$retval" | |
| subst $i "$t" | |
| local arg="$retval" | |
| push "$arg" | |
| push "$fun" | |
| app | |
| return | |
| fi | |
| case $leading in | |
| ''|*[!0-9]*) retval="$leading" ;; | |
| *) | |
| if [ "$leading" -eq "$i" ]; then | |
| retval="$t" | |
| else | |
| retval="$leading" | |
| fi | |
| esac | |
| } | |
| function eval() { | |
| pop | |
| local leading="$retval" | |
| if [ "$leading" = "U" ]; then | |
| pop | |
| local level="$retval" | |
| retval="U $level" | |
| return | |
| fi | |
| if [ "$leading" = "Π" ] || [ "$leading" = "λ" ]; then | |
| eval | |
| local type="$retval" | |
| eval | |
| local clos="$retval" | |
| retval="$leading $type $clos" | |
| return | |
| fi | |
| if [ "$leading" = "β" ]; then | |
| eval | |
| local fun="$retval" | |
| eval | |
| local arg="$retval" | |
| push "$arg" | |
| push "$fun" | |
| app | |
| return | |
| fi | |
| retval="$leading" | |
| } | |
| # Type checker | |
| function conv() { | |
| term | |
| local term1="$retval" | |
| local leading1=$(head "$term1") | |
| term | |
| local term2="$retval" | |
| local leading2=$(head "$term2") | |
| if ( [ "$leading1" = "β" ] && [ "$leading2" = "β" ] ) || | |
| ( [ "$leading1" = "Π" ] && [ "$leading2" = "Π" ] ) || | |
| ( [ "$leading1" = "λ" ] && [ "$leading2" = "λ" ] ); then | |
| push "$term1" | |
| pop | |
| term | |
| local arg11="$retval" | |
| term | |
| local arg12="$retval" | |
| push "$term2" | |
| pop | |
| term | |
| local arg21="$retval" | |
| term | |
| local arg22="$retval" | |
| push "$arg21" | |
| push "$arg11" | |
| conv | |
| local P=$retval | |
| push "$arg22" | |
| push "$arg12" | |
| conv | |
| local Q=$retval | |
| if [ "$P" = "true" ] && [ "$Q" = "true" ]; then | |
| retval=true | |
| else | |
| retval=false | |
| fi | |
| return | |
| fi | |
| if [ "$leading1" = "λ" ]; then | |
| push "$term1" | |
| pop | |
| term | |
| term | |
| local clos1="$retval" | |
| push "0" | |
| push "$term2" | |
| app | |
| local clos2="$retval" | |
| push "$clos2" | |
| push "$clos1" | |
| conv | |
| return | |
| fi | |
| if [ "$leading2" = "λ" ]; then | |
| push "$term2" | |
| pop | |
| term | |
| term | |
| local clos2="$retval" | |
| push "0" | |
| push "$term1" | |
| app | |
| local clos1="$retval" | |
| push "$clos2" | |
| push "$clos1" | |
| conv | |
| return | |
| fi | |
| if [ "$term1" = "$term2" ]; then | |
| retval=true | |
| else | |
| retval=false | |
| fi | |
| } | |
| function imax() { | |
| local level1="$1" | |
| local level2="$2" | |
| if [ "$level1" = "Z" ]; then | |
| echo $level2 | |
| return | |
| fi | |
| if [ "$level2" = "Z" ]; then | |
| echo $level1 | |
| return | |
| fi | |
| echo S$(imax "${level1:1}" "${level2:1}") | |
| } | |
| function infer() { | |
| pop | |
| local leading="$retval" | |
| local ctx=("$@") | |
| if [ "$leading" = "U" ]; then | |
| pop | |
| local level="$retval" | |
| retval="U S$level" | |
| return | |
| fi | |
| if [ "$leading" = "λ" ]; then | |
| term | |
| local type="$retval" | |
| term | |
| local clos="$retval" | |
| push "$type" | |
| infer "${ctx[@]}" | |
| if [ "$(head $retval)" != "U" ]; then | |
| echo “$type” expected to be a type. | |
| exit 1 | |
| fi | |
| push "$type" | |
| eval | |
| local newtype="$retval" | |
| push "$newtype" | |
| up | |
| local newctx=("$retval") | |
| for value in "${ctx[@]}"; do | |
| push "$value" | |
| up | |
| newctx+=("$retval") | |
| done | |
| push "$clos" | |
| infer "${newctx[@]}" | |
| retval="Π $newtype $retval" | |
| return | |
| fi | |
| if [ "$leading" = "Π" ]; then | |
| term | |
| local type="$retval" | |
| term | |
| local clos="$retval" | |
| push "$type" | |
| infer "${ctx[@]}" | |
| if [ "$(head $retval)" != "U" ]; then | |
| echo “$type” expected to be a type. | |
| exit 1 | |
| fi | |
| local level1=$(tail $retval) | |
| push "$type" | |
| eval | |
| push "$retval" | |
| up | |
| local newctx=("$retval") | |
| for value in "${ctx[@]}"; do | |
| push "$value" | |
| up | |
| newctx+=("$retval") | |
| done | |
| push "$clos" | |
| infer "${newctx[@]}" | |
| if [ "$(head $retval)" != "U" ]; then | |
| echo “$type” expected to be a type. | |
| exit 1 | |
| fi | |
| local level2=$(tail $retval) | |
| retval="U $(imax $level1 $level2)" | |
| return | |
| fi | |
| if [ "$leading" = "β" ]; then | |
| term | |
| local fun="$retval" | |
| term | |
| local arg="$retval" | |
| push "$fun" | |
| infer "${ctx[@]}" | |
| local funtype="$retval" | |
| if [ "$(head $funtype)" != "Π" ]; then | |
| echo “$fun” expected to be a function. | |
| exit 1 | |
| fi | |
| push "$arg" | |
| infer "${ctx[@]}" | |
| local argtype="$retval" | |
| push "$funtype" | |
| pop | |
| term | |
| local funtypearg="$retval" | |
| term | |
| local funtypeclos="$retval" | |
| push "$funtypearg" | |
| push "$argtype" | |
| conv | |
| if [ "$retval" != "true" ]; then | |
| echo $funtypearg ≠ $argtype | |
| exit 1 | |
| fi | |
| push "$arg" | |
| push "λ $funtypearg $funtypeclos" | |
| app | |
| return | |
| fi | |
| case $leading in | |
| ''|*[!0-9]*) | |
| if [[ -f "$leading" ]]; then | |
| retval=$(cat "$leading") | |
| else | |
| echo Unbound variable “$leading”. | |
| exit 1 | |
| fi ;; | |
| *) | |
| if [ "${ctx[$leading]+present}" ]; then | |
| retval=${ctx[$leading]} | |
| else | |
| echo Unbound variable “$leading” in context: ${ctx[@]} | |
| exit 1 | |
| fi | |
| esac | |
| } | |
| term="$*" | |
| if [ -z "$term" ]; then | |
| echo Usage: $0 [term] | |
| exit 1 | |
| fi | |
| ctx=() | |
| push "$term" | |
| infer "${ctx[@]}" | |
| echo INFER: $retval | |
| push "$term" | |
| eval | |
| echo EVAL: $retval |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment