experimental dependently typed programming language
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.




Welcome to the Midori Language! This language is an attempt (read work in progress) to introduce to the many fields of Engineering (mechanical, electrical, industrial, etc...) a formal method to produce clean, machine checked code; for an imperative weakly\untyped close-to-the-hardware middle language.


  • Lambdas: unlike in many functional languages, the lambda's in Midori are explicitly delineated, to make the parser simpler, and to make it more explicit to the programmer which function has which scope. unfortunately, this also clutters up the view for many simple lambdas. syntactic sugar will probably be added latter to resolve this.

    (x:type)(i:x){ i }

    the above term has the type:

    (x:type) -> x -> x
  • Definitions: definitions are the only way to introduce named functions at the moment. they are implemented as explicit substitutions, and have pseudo parameters. (pseudo, in that they are actually parameters to a lambda function, not to the substitution)

    id (x:type)(i:x) : x { i } 
  • Local Functions: explicit scope of the definitions, and their use will hopefully keep scoping easy to track.

    idExample : Integer {
      let id (x:type)(i:x) : x { i } 
          seven : Integer { 7 } 
      { id 7 }
  • Modules: Modules consist of a series of definitions, and symbols. Free variables of the module must be stated in in import list after the name of the module ("import ... "). Imported definitions can be renamed to a different name to avoid name clashes via the use of a qualified import ("import ... qualified ..."). When a variable is qualified the variable's name is prepended with the name used in the qualified import, and a dot separating them, I.E. below is a module that imports Boolean, and qualifies all variables with "Bool", so "Boolean" becomes "Bool.Boolean" etc...

    module List
      import "Data/Bool" qualified Bool
  • Symbolic Syntax: Symbolic syntax is parsed and expaneded before typechecking, and is handled via an operator- precedence parser. a few symbols are restricted ("->", ":", "{", "}", "\", "*", "(", ")", "?", "=") negative fixity implies left association, (fixity is the integer after the pattern clause). Pattern clauses are essentially strings, and are composed of untyped terminals, which consist of either valid identifiers or operators, and single quoted non-terminals that must be valid identifiers. Pattern clauses have only one real restriction at the moment: patterns consist of a list of terminals seperated and optionally ended by non-terminals, or a list of non-terminals seperated and optionally ended by terminals. The restriction is to help guarantee that parsing of symbolic notations terminates without any parsing errors.

    syntax "'x' + 'y'" fixity 5 let (x:Real) (y:Real) { add x y }
    syntax "'a' $ 'x' :: 'xs'" fixity 4 let (a:type) (x:a) (xs:List a) { Cons a x xs }