Recursion is not an option.
An implementation of the Mugda paper -- "Termination Checking for a Dependently Typed Language", 2007, by Karl Mehltretter.
The "Mu" of the name "Mugda" comes from μ-operator (mu-operator) of general recursive function.
When using zero arity data constructor, we must write them in ().
For example, zero and (zero) are the same.
But when using zero arity data constructor in pattern, we must write them in ().
For example, we should not write zero but write (zero),
otherwise the interpreter can not distinguish pattern variable
from this zero arity data constructor.
The syntax of inductive datatype definition -- (data),
is learnt from "The Little Typer".
Install it by the following command:
npm install -g @xieyuheng/mugdaThe command-line program is called mu.
open a REPL:
mu replor just:
muRun a file:
mu run tests/basic/id.test.muRun a file and watch file change:
mu run tests/basic/id.test.mu --watchPlease see tests/ and std/ for more examples.
(data Boolean () ()
[true () Boolean]
[false () Boolean])
(fn if (Pi ([A Type]) (-> Boolean A A A))
[(A (true) a b) a]
[(A (false) a b) b])
(define and (-> Boolean Boolean Boolean)
(lambda (a b)
(if Boolean a b false)))
(define or (-> Boolean Boolean Boolean)
(lambda (a b)
(if Boolean a true b)))
(and true true)
(and true false)
(and false true)
(and false false)
(or true true)
(or true false)
(or false true)
(or false false)(data Nat () ()
[zero () Nat]
[add1 ([prev Nat]) Nat])
(fn add (-> Nat Nat Nat)
[(x (zero)) x]
[(x (add1 y)) (add1 (add x y))])
add
(add (add1 zero))
(add (add1 zero) (add1 zero))(data List ([+ A Type]) ()
[null () (List A)]
[cons ([head A] [tail (List A)]) (List A)])
(import "../nat/index.mu" Nat zero add1)
(fn length (Pi ([A Type]) (-> (List A) Nat))
[(A (null A)) zero]
[(A (cons A head tail)) (add1 (length A tail))])
(length Nat (null Nat))
(length Nat (cons Nat zero (null Nat)))
(length Nat (cons Nat zero (cons Nat zero (null Nat))))npm install # Install dependencies
npm run build # Compile `src/` to `lib/`
npm run build:watch # Watch the compilation
npm run format # Format the code
npm run test # Run test
npm run test:watch # Watch the testingThank you, Karl Mehltretter, for writing this paper.