print :: string -> string * top string .
Indeed, the following is a valid code of Neut:(ensure core/ “”) (include “core/”) (with identity.bind (let str “a”) (let _ (string.print &str)) (let _ (string.print &str)) (let _ (string.print &str)) top.unit) ; ~> top.unitOr,(ensure core/ “”) (include “core/”) (with identity.bind (let str “a”) (let _ (string.print &str)) (let _ (string.print &str)) (string.print str)) ; ~> (unit, “a”)This notation is “borrowing” in Neut.
Example(inductive list ((a tau)) (nil () (list a)) (cons ((_ a) (_ (list a))) (list a))) (define length ((a tau) (xs (list a))) ( i64 a xs (λ () 0) (λ (_ ys) (add-i64 1 (length a ys))))) (let xs (list.cons * 10 (list.cons * 20 (list.nil i64)))) (i64.print (length xs)) ; ~> 2 ; mutually inductive types (inductive (even ((_ (nat))) (zero-is-even () (even ( (succ-of-odd-is-even ((n (nat)) (_ (odd n))) (even (nat.succ n)))) (odd ((_ (nat))) (succ-of-even-is-odd ((n (nat)) (_ (even n))) (odd (nat.succ n)))))Syntax(inductive LEAF ((LEAF TREE) … (LEAF TREE)) (LEAF ((LEAF TREE) … (LEAF TREE)) TREE) … (LEAF ((LEAF TREE) … (LEAF TREE)) TREE)) ; n-mutual inductive type (inductive (LEAF ((LEAF TREE) … (LEAF TREE)) (LEAF ((LEAF TREE) … (LEAF TREE)) TREE) … (LEAF ((LEAF TREE) … (LEAF TREE)) TREE)) … (LEAF ((LEAF TREE) … (LEAF TREE)) (LEAF ((LEAF TREE) … (LEAF TREE)) TREE) … (LEAF ((LEAF TREE) … (LEAF TREE)) TREE)))SemanticsWhen parsed, the inductive statement is translated into the let statements that defines (1) the inductive type, (2) the introduction rules (or the constructors of the inductive type), and (3) the pattern match function.
Example(introspect OS (linux (include library “constant/linux.neut”)) (darwin (include library “constant/darwin.neut”)))Syntax(introspect LEAF (LEAF TREE … TREE) … (LEAF TREE … TREE))Semantics(introspect VAR (VAR-1 stmt-1-1 … stmt-1-n{1}) … (VAR-m stmt-m-1 … stmt-m-n{m})) ~> (stmt-i-1) … (stmt-i-n) [where VAR == VAR-i]If the corresponding value is not found in the clause list, this statement does nothing.
For example, the code(define fact ((x i64)) (witness i64 (if (icmp-sle-i64 x 0) 1 (mul-i64 x (fact (sub-i64 x 1))))))is preferred to:(define fact ((x i64)) (if (icmp-sle-i64 x 0) 1 (mul-i64 x (fact (sub-i64 x 1)))))fixfix is for recursion.

Comments to: u2zv1wx/neut: A dependently-typed programming language with compile-time malloc/free determination

Your email address will not be published. Required fields are marked *

Attach images - Only PNG, JPG, JPEG and GIF are supported.


Welcome to Typer

Brief and amiable onboarding is the first thing a new user sees in the theme.
Join Typer
Registration is closed.