Ntha
所属分类：collect
开发工具：Haskell
文件大小：0KB
下载次数：0
上传日期：2016-11-17 14:29:10
上 传 者：
sh-1993
说明： Ntha编程语言，
(The Ntha Programming Language,)
文件列表:
.travis.yml (1076, 2016-11-17)
LICENSE (1519, 2016-11-17)
Paths_ntha.hs (93, 2016-11-17)
Setup.hs (46, 2016-11-17)
app/ (0, 2016-11-17)
app/Main.hs (3445, 2016-11-17)
examples/ (0, 2016-11-17)
examples/kanren.ntha (4283, 2016-11-17)
examples/misc.ntha (3430, 2016-11-17)
examples/module.ntha (208, 2016-11-17)
examples/symbolic_computation.ntha (6413, 2016-11-17)
examples/type_infer.ntha (7836, 2016-11-17)
lib/ (0, 2016-11-17)
lib/std.ntha (3734, 2016-11-17)
ntha.cabal (3324, 2016-11-17)
runexample.sh (179, 2016-11-17)
screenshot.gif (80753, 2016-11-17)
src/ (0, 2016-11-17)
src/Ntha.hs (546, 2016-11-17)
src/Ntha/ (0, 2016-11-17)
src/Ntha/Core/ (0, 2016-11-17)
src/Ntha/Core/Ast.hs (7522, 2016-11-17)
src/Ntha/Core/Prelude.hs (4091, 2016-11-17)
src/Ntha/Parser/ (0, 2016-11-17)
src/Ntha/Parser/Lexer.x (3705, 2016-11-17)
src/Ntha/Parser/Parser.y (17061, 2016-11-17)
src/Ntha/Runtime/ (0, 2016-11-17)
src/Ntha/Runtime/Eval.hs (12706, 2016-11-17)
src/Ntha/Runtime/Value.hs (5318, 2016-11-17)
src/Ntha/State.hs (887, 2016-11-17)
src/Ntha/Type/ (0, 2016-11-17)
src/Ntha/Type/Infer.hs (12520, 2016-11-17)
src/Ntha/Type/Refined.hs (5937, 2016-11-17)
src/Ntha/Type/Type.hs (9167, 2016-11-17)
src/Ntha/Type/TypeScope.hs (1217, 2016-11-17)
src/Ntha/Z3/ (0, 2016-11-17)
src/Ntha/Z3/Assertion.hs (2128, 2016-11-17)
... ...
# Ntha Programming Language
[](https://travis-ci.org/zjhmale/Ntha)
[](https://github.com/zjhmale)
[](https://en.wikipedia.org/wiki/Haskell_(programming_language))
[](https://hackage.haskell.org/package/ntha)
[](https://hackage.haskell.org/package/ntha)
a tiny statically typed functional programming language.
## Installation
* brew install z3
* cabal install ntha
## Features
* Global type inference with optional type annotations.
* Lisp flavored syntax with Haskell like semantic inside.
* Support basic types: Integer, Character, String, Boolean, Tuple, List and Record.
* Support unicode keywords.
* Support destructuring.
* ADTs and pattern matching.
* Haskell like type signature for type checking.
* Refined types (still in early stage, just support basic arithmetic operations and propositinal logic, [here is some examples](https://github.com/zjhmale/Ntha/blob/master/examples/misc.ntha#L188-L195)), based on [z3-encoding](https://github.com/izgzhen/z3-encoding/tree/1d794c10db716ac9308e49bf4f5a115e14212f31)
* Module system (still in early stage, lack of namespace control).
* Support pattern matching on function parameters.
* Lambdas and curried function by default.
* Global and Local let binding.
* Recursive functions.
* If-then-else / Cond control flow.
* Type alias.
* Do notation.
* Begin block.
## Future Works
* Atoms (need to handle mutable state in evaluation procedure, reference to the [implementation of Clea Programming Language](https://github.com/zjhmale/Clea/blob/master/src/Prologue.hs#L191-211)).
* error propagation (try / catch).
* Lazyness.
* JIT backend.
* Type-classes (desuger to Records).
* Rank-N types ([a naive implementation of First-Class Polymorphism](https://github.com/zjhmale/HMF/tree/master/src/FCP)).
* λπ
* Fully type checked lisp like macros (comply with the internal design of Template Haskell).
* TCO.
## Screenshot
## Example
```Clojure
(type Name String)
(type Env [(Name . Expr)])
(data Op Add Sub Mul Div Less Iff)
(data Expr
(Num Number)
(Bool Boolean)
(Var Name)
(If Expr Expr Expr)
(Let [Char] Expr Expr)
(LetRec Name Expr Expr)
(Lambda Name Expr)
(Closure Expr Env)
(App Expr Expr)
(Binop Op (Expr . Expr)))
(let op-map {:add +
:sub -
:mul *
:div /
:less <
:iff =})
(arith-eval : (α → (β → Z)) → ((α × β) → (Maybe Expr)))
( arith-eval [fn (v1 . v2)]
(Just (Num (fn v1 v2))))
(logic-eval : (α → (β → B)) → ((α × β) → (Maybe Expr)))
( logic-eval [fn (v1 . v2)]
(Just (Bool (fn v1 v2))))
(let eval-op
(λ op v1 v2
(match (v1 . v2)
(((Just (Num v1)) . (Just (Num v2)))
(match op
(Add (arith-eval (:add op-map) (v1 . v2)))
(Sub (arith-eval (:sub op-map) (v1 . v2)))
(Mul (arith-eval (:mul op-map) (v1 . v2)))
(Div (arith-eval (:div op-map) (v1 . v2)))
(Less (logic-eval (:less op-map) (v1 . v2)))
(Iff (logic-eval (:iff op-map) (v1 . v2)))))
(_ Nothing))))
(eval : [(S × Expr)] → (Expr → (Maybe Expr)))
( eval [env expr]
(match expr
((Num _) (Just expr))
((Bool _) → (Just expr))
((Var x) (do Maybe
(val ← (lookup x env))
(return val)))
((If condition consequent alternative) →
(match (eval env condition)
((Just (Bool true)) → (eval env consequent))
((Just (Bool false)) → (eval env alternative))
(_ → (error "condition should be evaluated to a boolean value"))))
((Lambda _ _) → (Just (Closure expr env)))
((App fn arg) → (let [fnv (eval env fn)]
(match fnv
((Just (Closure (Lambda x e) innerenv)) →
(do Maybe
(argv ← (eval env arg))
(eval ((x . argv) :: innerenv) e)))
(_ → (error "should apply arg to a function")))))
((Let x e1 in-e2) (do Maybe
(v ← (eval env e1))
(eval ((x . v) :: env) in-e2)))
;; use fix point combinator to approach "Turing-complete"
((LetRec x e1 in-e2) → (eval env (Let "Y" (Lambda "h" (App (Lambda "f" (App (Var "f") (Var "f")))
(Lambda "f" (App (Var "h")
(Lambda "n" (App (App (Var "f") (Var "f"))
(Var "n")))))))
(Let x (App (Var "Y") (Lambda x e1))
in-e2))))
((Binop op (e1 . e2)) => (let [v1 (eval env e1)
v2 (eval env e2)]
(eval-op op v1 v2)))))
(begin
(print "start")
(let result (match (eval [] (LetRec "fact" (Lambda "n" (If (Binop Less ((Var "n") . (Num 2)))
(Num 1)
(Binop Mul ((Var "n") . (App (Var "fact")
(Binop Sub ((Var "n") . (Num 1))))))))
(App (Var "fact") (Num 5))))
((Just (Num num)) (print (int2str num)))
(Nothing (error "oops"))))
(print result)
(print "finish"))
```
## License
Copyright 2016 zjhmale
Distributed under the [](https://en.wikipedia.org/wiki/BSD_licenses)
近期下载者：
相关文件：
收藏者：