pinafore [-i|--interactive] [-n|--no-run] [--data PATH] [SCRIPT]
pinafore with one or more scripts containing actions to run those actions.
Each script must consist of an expression of a subtype of
By default, pinafore will store local information in the directory
$XDG_DATA_HOME/pinafore (or else
--data to specify a different directory.
To just parse and type-check a file without running it, use
pinafore is invoked with
--interactive, it will run in interactive mode.
This may be particularly helpful for understanding the type system.
At the prompt, you can enter:
- An expression. If this is an action, it will be executed, otherwise its value will be printed.
- A let-expression, which will add bindings to the context.
- A special command:
- ":type expression" will show the inferred type of an expression.
- ":simplify+ type" will show a simplified positive type.
- ":simplify- type" will show a simplified negative type.
<interactive> element in the grammar.
Here's an example:
pinafore> 3 + 4 7 pinafore> let p = [5,6,7] ++ [1,1,1] pinafore> let f x = x ++ x pinafore> :type f : [a] -> [a] pinafore> f p [5, 6, 7, 1, 1, 1, 5, 6, 7, 1, 1, 1] pinafore> :simplify+ (a -> Literal) | ((Text & b) -> a) (a & Text) -> Literal | a