Use metavariables instead of overloading type variables.
Use less bad method for storing constructor types.
Add algebraic data types.
Ivo (IPA: /aɪvoʊ/) is a programming language based on the Hindley-Milner type system plus undelimited control (call/cc).
You may run the Ivo interpreter using cabal run [-- args...]
or
by installing it to your path with cabal install
.
For information about ivo
's command line arguments, please refer to ivo --help
(or stack run -- --help
).
Type in your command, definition, or expression at the prompt: >>
.
Expressions will be typechecked, evaluated using call-by-value, and then printed.
Exit the prompt with Ctrl-d
(or equivalent).
These commands are available:
:clear
: Clear all of your variable definitions.
:load <filename>
:
Execute a file containing Ivo definitions and expressions in the interpreter. Variables already defined in the interpreter will be defined in the file; variables defined by the file will be defined in the interpreter.
The filename may contain spaces, but trailing whitespace will be trimmed.
:printTypes <both/decls/exprs/off>
:
Print to STDERR the inferred types of top-level declarations, of expressions entered into the interpreters, of both, or of neither.
This setting defaults to off
.
:trace <off/local/global>
:
If the argument is local
, intermediate expressions will be printed
as they are evaluated;
If the argument is global
, the entire expression will be printed
with each evaluation step.
The default value is off
.
The parser's error messages currently are virtually useless, so be very careful with your syntax.
f x y
\x y z. E
or λx y z. E
let x = E; y = F in G
let undefined = undefined in undefined
.(E)
()
, (x, y)
(or (,) x y
), Left x
, Right y
, Z
, S
, []
, (x :: xs)
(or (:) x xs
), Char n
.
Char
takes a natural number and turns it into a character.{ Left a -> e ; Right y -> f }
{ Z -> x, S -> y } 10
reduces to y
.(x :: xs)
and not ((::) x xs)
.1234
, [e, f, g, h]
, 'a
, "abc"
// line comment
, /* block comment */
Top-level contexts (e.g. the REPL or a source code file)
allow declarations (let x = E
without multiple definitions in ...
),
which make your definitions available for the rest of the program's execution.
You must separate your declarations and expressions with ;
.
Types are checked/inferred using the Hindley-Milner type inference algorithm.
a -> b
(constructed by \x. e
)a * b
(constructed by (x, y)
)★
(constructed by ()
)a + b
(constructed by Left x
or Right y
)⊥
(currently useless because incomplete patterns are allowed)Nat
(constructed by Z
and S
)List a
(constructed by []
and (x :: xs)
)Char
(constructed by Char
, which takes a Nat
)∀a b. t
Builtins are variables that correspond with a built-in language feature that cannot be replicated by user-written code. They still are just variables though; they do not receive special syntactic treatment.
callcc : ∀a b. (((a -> b) -> a) -> a)
:
the call-with-current-continuation control flow operator.Continuations are printed as λ!. ... ! ...
, like a lambda abstraction
with an argument named !
which is used exactly once;
however, continuations are not the same as lambda abstractions
because they perform the side effect of modifying the current continuation,
and this is not valid syntax you can enter into the REPL.
You can see some example code in examples/examples.ivo
.