|
3 years ago | |
---|---|---|
.github/workflows | 3 years ago | |
app | 3 years ago | |
examples | 3 years ago | |
src | 3 years ago | |
test | 3 years ago | |
.editorconfig | 3 years ago | |
.gitignore | 4 years ago | |
LICENSE | 4 years ago | |
README.md | 3 years ago | |
Setup.hs | 4 years ago | |
package.yaml | 3 years ago | |
stack.yaml | 3 years ago | |
stack.yaml.lock | 3 years ago |
README.md
The Ivo Programming Language
Ivo (IPA: /aɪvoʊ/) is a programming language intended as a tool for its author to explore interesting programming language features.
Ivo is currently in a very early stage of development and most likely is not of any practical or academic interest; however, that may change in the future. This README serves to document the language as it currently stands, not what the language one day hopes to be.
Using the Ivo interpreter
You may run the Ivo interpreter (ivo
)
by installing it to your local path using stack install
,
or equivalently, using stack run [-- args...]
.
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).
Interpreter commands
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 Ivo language
Syntax
The parser's error messages currently are virtually useless, so be very careful with your syntax.
- Variable names: any sequence of letters.
- Function application:
f x y
- Lambda abstraction:
\x y z. E
orλx y z. E
- Let expressions:
let x = E; y = F in G
- The definitions of let expessions may be recursive:
let undefined = undefined in undefined
.
- The definitions of let expessions may be recursive:
- Parenthetical expressions:
(E)
- Constructors:
()
,(x, y)
(or(,) x y
),Left x
,Right y
,Z
,S
,[]
,(x :: xs)
(or(:) x xs
),Char n
.- The parentheses around the cons constructor are not optional.
Char
takes a natural number and turns it into a character.
- Pattern matchers:
{ Left a -> e ; Right y -> f }
- Pattern matchers can be applied like functions, e.g.
{ Z -> x, S -> y } 10
reduces toy
. - Patterns must use the regular form of the constructor, e.g.
(x :: xs)
and not((::) x xs)
. - There are no nested patterns or default patterns.
- Incomplete pattern matches will crash the interpreter.
- Pattern matchers can be applied like functions, e.g.
- Literals:
1234
,[e, f, g, h]
,'a
,"abc"
- Strings are represented as lists of characters.
- Type annotations: there are no type annotations; types are inferred only.
- Comments:
// 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
Types are checked/inferred using the Hindley-Milner type inference algorithm.
- Functions:
a -> b
(constructed by\x. e
) - Products:
a * b
(constructed by(x, y)
) - Unit:
★
(constructed by()
) - Sums:
a + b
(constructed byLeft x
orRight y
) - Bottom:
⊥
(currently useless because incomplete patterns are allowed) - The natural numbers:
Nat
(constructed byZ
andS
) - Lists:
List a
(constructed by[]
and(x :: xs)
) - Characters:
Char
(constructed byChar
, which takes aNat
) - Universal quantification (forall):
∀a b. t
Builtins
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.
Example code
You can see some example code in examples/examples.ivo
.