The ntha package

[Tags:bsd3, library, program, test]

Check out the readme for documentation.

[Skip to Readme]


Versions 0.1.0, 0.1.1, 0.1.3
Dependencies array, base (>=4.7 && <5), containers, haskeline, lens, monad-loops, mtl (==2.2.*), ntha, pretty, z3 (>=4.1.0) [details]
License BSD3
Copyright 2016 zjhmale
Author zjhmale
Stability Unknown
Category Compiler , Language
Home page
Source repository head: git clone
Uploaded Sat Aug 27 06:21:39 UTC 2016 by zjhsdtc
Distributions NixOS:0.1.3
Downloads 81 total (4 in the last 30 days)
0 []
Status Docs not available [build log]
All reported builds failed as of 2016-11-20 [all 3 reports]


  • Ntha
    • Core
      • Ntha.Core.Ast
      • Ntha.Core.Prologue
    • Parser
      • Ntha.Parser.Lexer
      • Ntha.Parser.Parser
    • Runtime
      • Ntha.Runtime.Eval
      • Ntha.Runtime.Value
    • Ntha.State
    • Type
      • Ntha.Type.Infer
      • Ntha.Type.Refined
      • Ntha.Type.Type
      • Ntha.Type.TypeScope
    • Z3
      • Ntha.Z3.Assertion
      • Ntha.Z3.Class
      • Ntha.Z3.Context
      • Ntha.Z3.Encoding
      • Ntha.Z3.Logic


Maintainer's Corner

For package maintainers and hackage trustees

Readme for ntha

Readme for ntha-0.1.3

Ntha Programming Language

Build Status zjhmale Haskell Hackage Hackage-Deps

a tiny statically typed functional programming language.


  • brew install z3
  • cabal install ntha


  • 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), based on z3-encoding
  • 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




(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))
    ((Binop op (e1 . e2)) => (let [v1 (eval env e1)
                                   v2 (eval env e2)]
                               (eval-op op v1 v2)))))

  (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"))


Copyright © 2016 zjhmale

Distributed under the license BSD