File	Date	Author	Commit
Midori	2013-02-20	James M.	[ab662e] improved syntax, rewrite using bnfc again, beca...
COPYING	2012-08-25	James M.	[5468d7] pre-alpha
LICENSE	2012-08-25	James M.	[5468d7] pre-alpha
Midori.cabal	2012-12-12	James M.	[87612f] removed documentation for now, introduced more ...
README	2012-12-10	listofoptions	[e51ca9] Update README
README.md	2013-02-20	James M.	[ab662e] improved syntax, rewrite using bnfc again, beca...
TODO	2012-12-17	listofoptions	[6b7c69] Update TODO

Read Me

Midori
======

Introduction:
-------------

  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. The need for such a language is (IMHO) huge, as an 
  example take PLCs: (programmable logic controllers) with archaic, messy, system specific dialects of (so called) 
  languages like FBD, and ladder logic; controlling huge multi-million dollar machines in cannot-fail setups without any 
  form of safety besides a simulator that might catch some errors. Luckily the industries seem to be moving towards 
  languages like VHDL, and .NET for some safety, though with viruses like STUXNET popping out of the woodwork, these 
  Turing complete languages can only offer safety up to a certain point. Midori is not Turing complete, so there should 
  be almost no vector of attack once the code generator for once a middle code  generator is formally verified (this 
  middle language can be any language: C, VHDL, C#, java, ETC...), though certain functionality will have to be emulated 
  (like non-terminating) with some low level tricks, I am confident that the boiler plate required for this will be 
  minimal, and can be checked for possible errors with minimal work.

Syntax:
-------

  * __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:*)(i: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:*) = {
          \(i:x) { x }
        } ```

  * __Local Functions:__ explicit scope of the definitions, and their use will hopefully keep scoping easy to track.

    ``` id (x:*) = {
          let id' (i:x) = {
                x
              }
          in {
            id'
          }
        } ```

  * __Modules:__ modules consist of a series of documentation, definitions, and symbols. free variables of the module
      must be stated in an assumption list after the name of the module (between "let", and "from"), along with
      the module that the variables are contained in. this is the only possible source of impurity in the language
      at the moment, because these assumptions are loaded directly into the type checker without checking the associated
      files first. the only reason we do this is to allow some form of separate compilation. when the current file is
      done compiling, we then compile the sub modules and check against the type given in the parent’s type signature.

    ``` module list
          let (Bool:*) (True:Bool) (False:Bool) (if:(a:*) -> Bool -> a -> a) from "data/bool"
          in { ... } ```

  * __Documentation:__ documentation is inlined with the code, and ignored by the interpreter if not asked.

    ``` document "this is the identity function:" \(a:*) (x:a) { x } ```

  * __Symbolic Syntax:__ symbolic syntax is lifted before type checking. a few symbols are restricted
      ("->", ":", "{", "}", "\\", "*", "(", ")", "?", "=") negative fixity implies left association,
      (fixity is the number after the string) free variables in the string must be valid identifiers, and be typed.

    ``` symb "x + y" 5 (x y: Integer) { add x y } ```