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 @cicada-lang/mugda
The command-line program is called mu
.
open a REPL:
mu repl
or just:
mu
Run a file:
mu run tests/basic/id.test.mu
Run a file and watch file change:
mu run tests/basic/id.test.mu --watch
Please 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 testing
Thank you, Karl Mehltretter, for writing this paper.
To make a contribution, fork this project and create a pull request.
Please read the STYLE-GUIDE.md before you change the code.
Remember to add yourself to AUTHORS. Your line belongs to you, you can write a little introduction to yourself but not too long.