Phox is a small functional programming language with:
- Hindley–Milner type inference,
- algebraic data types,
- pattern matching,
- multi-parameter typeclasses (
trait/impl), - requires (trait-bounds) inference,
- generic function template (
*let), - automatic type/trait resolution without type-annotation,
- iterator / generator pipeline,
- Rust-like module system,
- and more.
It aims to be a simple yet expressive tool - your clever companion for exploring type theory and practical programming.
Note
Phox is still under active development.
While most I/O primitives have not yet been implemented, but the following core features are already available:
- Type-level Unicode String Framework (
ScalarString, UTF-8, etc.) - Pretty-Printing Combinators
- Rich pure-functional core libraries (iter, array, fmt, ...)
- Experimental
print,println,eprint, andeprintln
See also https://mori0091.github.io/phox-book/
New to Phox? Start with 🚀 Getting Started.
- Hindley–Milner type inference
No need to annotate types in most cases.
(Phox includes a minimal type-annotation syntax for expressions, used only when disambiguation is needed.) - Algebraic data types (ADT)
Define expressive data structures with variants. - Pattern matching
Concise and powerful destructuring. - Newtype shorthand
Cleaner syntax for single-constructor wrapper types. - First-class functions
Functions are values, operators are functions too. - Generic function templates
Non-first class / overloadable generic function templates. - Multi-parameter typeclasses (
trait/impl)
Define the relationship between multiple methods and multiple types. - Trait record
Typeclasses (trait/impl) can be instantiated as a first-class record value, with a simple syntax. - Module system
Rust like module / namespace definition. - Simple syntax
Inspired by ML-family languages, with a focus on clarity.
- In code examples,
// =>shows the result as a comment.- In REPL examples,
=>shows the evaluated result.
;separates multiple items (type declarations / statements / expressions) in a block or at the top level.- Each item is evaluated in order; only the last expression's value is returned.
- If a block or top-level input ends with
;, an implicit()is added.
// Multiple items in a block
{
let x = 1; // => (): () (discarded)
let y = 2; // => (): () (discarded)
x + y; // => 3: Int (discarded)
2 * x + y // => 4: Int (result)
}
// => 4: Int// Multiple items in the top level
let x = 1; // => (): () (discarded)
let y = 2; // => (): () (discarded)
x + y; // => 3: Int (discarded)
2 * x + y // => 4: Int (result)
// => 4: Int// Items in a block ends with `;`
{
1 + 2; // => 3: Int (discarded)
}
// => (): ()// Items in the top level ends with `;`
1 + 2; // => 3: Int (discarded)
// => (): ()// No items in a block
{}
// => (): ()type Option a = Some a | None;
type Pair a b = Pair a b;
type Result e a = Ok a | Err e;- Variants can take 0 or more arguments.
- Newtype shorthand is available when:
- There is only one variant, and
- The type name and constructor name are the same, and
- The variant has exactly one tuple, one record, or one array argument.
// Normal form
type Point a = Point @{ x: a, y: a };
// Newtype shorthand
type Point a = @{ x: a, y: a };
type Wrapper a = (a,);match (opt) {
Some x => x,
None => 0
}let t = (1, true, ());
let r = @{ x = 10, y = 20 };
let a = @[1, 2, 3];
(t.1, r.x, a[0]) // tuple index and array index is 0-based
// => (true, 10, 1): (Bool, Int, Int)👉 Field access is also available for newtype shorthand types.
type Point a = @{ x: a, y: a };
let p = Point @{ x = 3, y = 4 };
p.x + p.y
// => 7: Inttype Point a = (a, a);
let p = Point (3, 4);
p.0 + p.1
// => 7: Inttype Point a = @[a];
let p = Point @[3, 4];
p[0] + p[1]
// => 7: IntFunction f(x) = x + x can be defined like this:
let f = λx. 0 + x + x;
// let f = \x. 0 + x + x; // same as the above.
f 3
// => 6: Intlet normSq = λx.λy. 0 + x * x + y * y;
(normSq 2 3, 3 `normSq` 4)
// => (13, 25): (Int, Int)- Infix notation with backticks allows any function to be used as an operator.
Note
Why we use 0 + ... ?
Because primitive operators such as + are overloaded monomorphic functions.
👉 For more details (with Japanese explanations), see :
Once again, the function f(x) = x + x can also be defined as follows:
let f = λx. (x + x): Int;
f 3
// => 6: Int-
Optional type annotations for expressions (
expr: T) are available.
This adds atype_eq(type equality) constraint between the inferred type and the annotated type.
This helps type inference and the constraint solver resolve the last mile of ambiguity. -
Type annotations as signatures are required only in
traitdeclarations.
Other bindings (such asletand lambda parameters) do not accept type signatures.
Note
The expr: T syntax is only permitted for atomic expressions.
If you need to type-annotate a complex expression,
enclose the expression in parentheses and follow it with the type annotation.
// User-defined operator
let rec (**) = λx.λy.
if (0 >= y) 1
else x * x ** (y - 1);
((**) 2 3, 3 ** 4)
// => (8, 81): (Int, Int)- User-defined operators and also Built-in operators like
==, can always be used both infix and prefix.
(==) 1 1 // => true: Bool
1 == 1 // => true: Bool(-) 3 1 // => 2: Int (binary minus as a function)
negate 3 // => -3: Int (unary minus as a function)let x = 3;
-x // => -3: Int (unary minus; syntax sugar of `negate x`)! true // => false: Bool (unary not)
(!) true // => false: Bool (unary not; prefix form of `!`)
not true // => false: Bool (unary not)Phox provides pipeline operators and composition operators to make function application and chaining more readable.
They allow you to express nested calls as a clear flow of data or a sequence of transformations.
x |> fis the same asf x.f <| xis also the same asf x.- Use
|>when you want to read left‑to‑right, and<|when you prefer right‑to‑left.
x |> f |> g // g (f x)
g <| f <| x // g (f x)f >> gcreates a function that appliesffirst, theng.f << gcreates a function that appliesgfirst, thenf.
(f >> g) x // g (f x)
(f << g) x // f (g x)- Composition operators
>>/<<bind more tightly than pipeline operators. - Among pipelines,
|>binds more tightly than<|.
x |> f >> g // x |> (f >> g)
f <| x |> g // f <| (x |> g)let f = \x. x + 1;
let g = \x. x * 2;
let h = \x. x * x;
1 |> f |> g |> h; // => 16: Int ; h (g (f 1))
1 |> f >> g >> h; // => 16: Int ; h (g (f 1))
f >> g >> h <| 1; // => 16: Int ; h (g (f 1))
f >> g >> h <| 1 |> f; // => 36: Int ; h (g (f (f 1)))👉 In short: use pipelines to pass data, and composition to connect functions. You can freely combine both styles to write in the way that feels most natural.
Assuming that op is a arbitrary infix-operator:
|(e op)or|(e op _)are same as\rhs. e op rhs(bind the 1st argument ofopwithe)|(op e)or|(_ op e)are same as\lhs. lhs op e(bind the 2nd argument ofopwithe)
let f = |(1 +);
f 2 // 1 + 2
// => 3let f = |(/ 2);
f 6 // 6 / 2
// => 3let fact = \n. {
let init = (1, n);
let predicate = \(_, n'). 0 < n';
let update = \(a, n'). (a * n', n' - 1);
let (res, _) = for init predicate update;
res
};
fact 5
// => (120, 0): (Int, Int)while pred upd is same as \init. for init pred upd.
Phox supports traits (trait; similar to type classes) to define shared behavior across types.
trait Eq2 a {
eq : a -> a -> Bool;
neq : a -> a -> Bool;
}An implementation (impl) provides concrete definitions for a trait and a type:
impl Eq2 Int {
eq = λx.λy. @{Eq Int}.(==) x y;
neq = λx.λy. @{Eq Int}.(!=) x y;
};
impl Eq2 Bool {
eq = λx.λy. @{Eq Bool}.(==) x y;
neq = λx.λy. @{Eq Bool}.(!=) x y;
};Now you can use eq and neq with Int or Bool values:
eq 2 2 // => true
eq 2 3 // => false
neq 2 3 // => true
eq true true // => true
eq true false // => false
neq true true // => false
2 `eq` 2 // => true (infix notation)
2 `eq` 3 // => falseA trait record is a first-class value representing a trait implementation.
You can explicitly pass or select an implementation:
let eqInt = @{Eq Int}; // trait record for `Eq Int`
eqInt.(==) 2 3 // => false
2 `eqInt.(==)` 3 // => falseTrait records make resolution explicit and predictable.
If multiple candidates exist, ambiguity is reported as an error, and you can disambiguate by using a trait record.
👉 For more examples (with Japanese explanations), see トレイト利用例 (チートシート).
Arrays itself is also an iterator.
fold consumes all inputs and performs folding function.
@[1,2,3,4,5] |> fold (*) 1
// => 120: Intcounter generates infinite sequence of integers.
counter 1 |> take 5 |> fold (*) 1
// => 120: Intfilter filters elements by predicate function.
collect consumes all inputs and built result.
counter 1 |> filter (|(% 2) >> |(== 0)) |> take 5 |> collect Nil
// => Cons 2 (Cons 4 (Cons 6 (Cons 8 (Cons 10 Nil)))): List Intcounter 1 |> filter (|(% 2) >> |(== 0)) |> take 5 |> collect @[]
// => @[2, 4, 6, 8, 10]: @[Int]The ::core::iter module provides much more iterators / iterator-adapters, such as zip, zip_with, enumerate, etc.
👉 For more details, see also ::core::iter module.
Phox arrays (@[a]) are pure functional, reference-transparent, and support O(1) slicing with copy‑on‑write append.
They behave like immutable vectors with a clean, orthogonal API.
push @[1,2,3] 4
// => @[1, 2, 3, 4]: @[Int]
pop @[1,2,3]
// => Some (@[1, 2], 3): Option (@[Int], Int)
uncons @[1,2,3]
// => Some (1, @[2, 3]): Option (Int, @[Int])
collect @[1,2,3] @[4,5,6]
// => @[1, 2, 3, 4, 5, 6]: @[Int]
collect @[1,2,3] <| Cons 10 <| Cons 20 <| Cons 30 Nil
// => @[1, 2, 3, 10, 20, 30]: @[Int]
@[10, 20, 30] |> collect @[1,2,3]
// => @[1, 2, 3, 10, 20, 30]: @[Int]
(Cons 10 <| Cons 20 <| Cons 30 Nil) |> collect @[1,2,3]
// => @[1, 2, 3, 10, 20, 30]: @[Int]
insert1 @[1,2,3] 1 10
// => @[1, 10, 2, 3]: @[Int]
insertN @[1,2,3] 1 @[10,20]
// => @[1, 10, 20, 2, 3]: @[Int]
remove1 @[1,2,3,4] 1
// => @[1, 3, 4]: @[Int]
removeN @[1,2,3,4] 1 3
// => @[1, 4]: @[Int]
replace1 @[1,2,3,4] 1 10
// => @[1, 10, 3, 4]: @[Int]
replaceN @[1,2,3,4] 1 3 @[10,20,30]
// => @[1, 10, 20, 30, 4]: @[Int]👉 For more details, see also ::core::array module.
Phox can automatically select between safe and unsafe numeric conversions
using contextual multi-dispatch and type-directed constraint solving —
without any built-in notion of safety in the type system.
In other words:
Phox doesn’t know what “safe” means.
But the library design + trait resolution makes it emerge naturally.
counter 250
|> map cast
|> take_while ok?
|> map (\Ok x. x)
|> collect @[]: @[u8]
=> @[250, 251, 252, 253, 254, 255]: @[u8]counter 250
|> map @{TryCast a u8}.cast
|> take_while ok?
|> map (\Ok x. x)
|> collect @[]
=> @[250, 251, 252, 253, 254, 255]: @[u8](cast 10): u8
=> 10: u8
(cast 10): (Result e u8)
=> Ok 10: Result RuntimeError u8Advanced: full cast candidate list
> cast
ambiguous variable `cast`
candidates:
CodePoint -> Result RuntimeError ScalarValue requires TryCast CodePoint ScalarValue.
CodePoint -> u32 requires Cast CodePoint u32.
Int -> Result RuntimeError ScalarValue requires TryCast Int ScalarValue.
Int -> Result RuntimeError u16 requires TryCast Int u16.
Int -> Result RuntimeError u32 requires TryCast Int u32.
Int -> Result RuntimeError u64 requires TryCast Int u64.
Int -> Result RuntimeError u8 requires TryCast Int u8.
Int -> u16 requires Cast Int u16.
Int -> u32 requires Cast Int u32.
Int -> u64 requires Cast Int u64.
Int -> u8 requires Cast Int u8.
ScalarString -> @[u8] requires Cast ScalarString @[u8].
ScalarValue -> CodePoint requires Cast ScalarValue CodePoint.
ScalarValue -> u32 requires Cast ScalarValue u32.
u16 -> Int requires Cast u16 Int.
u16 -> Result RuntimeError Int requires TryCast u16 Int.
u16 -> Result RuntimeError u32 requires TryCast u16 u32.
u16 -> Result RuntimeError u64 requires TryCast u16 u64.
u16 -> Result RuntimeError u8 requires TryCast u16 u8.
u16 -> u32 requires Cast u16 u32.
u16 -> u64 requires Cast u16 u64.
u16 -> u8 requires Cast u16 u8.
u32 -> Int requires Cast u32 Int.
u32 -> Result RuntimeError CodePoint requires TryCast u32 CodePoint.
u32 -> Result RuntimeError Int requires TryCast u32 Int.
u32 -> Result RuntimeError ScalarValue requires TryCast u32 ScalarValue.
u32 -> Result RuntimeError u16 requires TryCast u32 u16.
u32 -> Result RuntimeError u64 requires TryCast u32 u64.
u32 -> Result RuntimeError u8 requires TryCast u32 u8.
u32 -> u16 requires Cast u32 u16.
u32 -> u64 requires Cast u32 u64.
u32 -> u8 requires Cast u32 u8.
u64 -> Int requires Cast u64 Int.
u64 -> Result RuntimeError Int requires TryCast u64 Int.
u64 -> Result RuntimeError u16 requires TryCast u64 u16.
u64 -> Result RuntimeError u32 requires TryCast u64 u32.
u64 -> Result RuntimeError u8 requires TryCast u64 u8.
u64 -> u16 requires Cast u64 u16.
u64 -> u32 requires Cast u64 u32.
u64 -> u8 requires Cast u64 u8.
u8 -> Int requires Cast u8 Int.
u8 -> Result RuntimeError Int requires TryCast u8 Int.
u8 -> Result RuntimeError u16 requires TryCast u8 u16.
u8 -> Result RuntimeError u32 requires TryCast u8 u32.
u8 -> Result RuntimeError u64 requires TryCast u8 u64.
u8 -> u16 requires Cast u8 u16.
u8 -> u32 requires Cast u8 u32.
u8 -> u64 requires Cast u8 u64.
∀ a. a -> Result RuntimeError a requires TryCast a a.
∀ a. a -> a requires Cast a a.
solution:
@{Cast CodePoint u32}.cast
@{Cast Int u16}.cast
@{Cast Int u32}.cast
@{Cast Int u64}.cast
@{Cast Int u8}.cast
@{Cast ScalarString @[u8]}.cast
@{Cast ScalarValue CodePoint}.cast
@{Cast ScalarValue u32}.cast
@{Cast a a}.cast
@{Cast u16 Int}.cast
@{Cast u16 u32}.cast
@{Cast u16 u64}.cast
@{Cast u16 u8}.cast
@{Cast u32 Int}.cast
@{Cast u32 u16}.cast
@{Cast u32 u64}.cast
@{Cast u32 u8}.cast
@{Cast u64 Int}.cast
@{Cast u64 u16}.cast
@{Cast u64 u32}.cast
@{Cast u64 u8}.cast
@{Cast u8 Int}.cast
@{Cast u8 u16}.cast
@{Cast u8 u32}.cast
@{Cast u8 u64}.cast
@{TryCast CodePoint ScalarValue}.cast
@{TryCast Int ScalarValue}.cast
@{TryCast Int u16}.cast
@{TryCast Int u32}.cast
@{TryCast Int u64}.cast
@{TryCast Int u8}.cast
@{TryCast a a}.cast
@{TryCast u16 Int}.cast
@{TryCast u16 u32}.cast
@{TryCast u16 u64}.cast
@{TryCast u16 u8}.cast
@{TryCast u32 CodePoint}.cast
@{TryCast u32 Int}.cast
@{TryCast u32 ScalarValue}.cast
@{TryCast u32 u16}.cast
@{TryCast u32 u64}.cast
@{TryCast u32 u8}.cast
@{TryCast u64 Int}.cast
@{TryCast u64 u16}.cast
@{TryCast u64 u32}.cast
@{TryCast u64 u8}.cast
@{TryCast u8 Int}.cast
@{TryCast u8 u16}.cast
@{TryCast u8 u32}.cast
@{TryCast u8 u64}.castPhox treats strings not as a single built-in primitive,
but as a family of types parameterized by what you consider a character.
All UTF-8 strings are guaranteed to be in canonical form at the type level.
-
CodePoint
Type of Unicode Code Point (may include surrogates) -
ScalarValue
Type of Unicode Scalar Value (surrogates excluded) -
ScalarString(synonym ofStr ScalarValue)
Type of UTF-8 strings (canonical UTF-8)
"Phox" |> collect @[]
// UTF-8 decode into Unicode scalar values
// => @['P', 'h', 'o', 'x']: @[ScalarValue]
@['P', 'h', 'o', 'x'] |> collect ""
// UTF-8 encode into ScalarString
// => "Phox": ScalarString
(cast "🎉🤣👍🍺"):@[u8]
// O(1) unwrap of the underlying UTF-8 bytes
// => @[240, 159, 142, 137, 240, 159, 164, 163, 240, 159, 145, 141, 240, 159, 141, 186]: @[u8]
counter 65 |> map cast |> take_while ok? |> map (\Ok sv. sv) |> take 5 |> collect ""
// Build a UTF-8 string from a numeric stream with no intermediate arrays
// => "ABCDE": ScalarString
collect "Hello " "World!"
// Concatenate UTF-8 strings
// => "Hello World!": ScalarStringThe ::core::fmt module provides a difference-list–based pretty-printing combinator library.
Pretty a defines the minimal primitive for formatting a value a into a ScalarString.
All higher-level formatting is expressed through combinator composition.
👉 For more details, see also ::core::fmt module.
trait Pretty a {
pp : ScalarString -> a -> ScalarString;
};
*let show = @{Pretty a}.pp "";Note
The ::core::fmt module is not imported by default.
You must either:
- call functions with a module path such as
fmt::show, or - explicitly import the module with
use ::core::fmt::*;
All examples below assume use ::core::fmt::*; has already been performed.
show <| paren 123
// => "(123)": ScalarString
show <| brace 123
// => "{123}": ScalarString
show <| bracket 123
// => "[123]": ScalarString
show <| prefix "@" "value"
// => "@value": ScalarString
show <| suffix "!!" "value"
// => "value!!": ScalarString
show <| enclose "<<" ">>" "value"
// => "<<value>>": ScalarStringshow <| sep_by ", " @[1, 2, 3]
// => "1, 2, 3": ScalarStringshow <| lpad 8 '_' "abc"
// => "_____abc": ScalarString
show <| rpad 8 '_' "abc"
// => "abc_____": ScalarString
show <| pad 8 '_' '/' "abc"
// => "__abc///": ScalarStringshow <| digits 100u8
// => "100": ScalarString
show <| hex-digits 200u8
// => "C8": ScalarString
show <| hex 100
// => "0x64": ScalarStringshow <| hex-dump @[10u8, 100u8, 200u8]
// => "0A 64 C8": ScalarString
show <| hex-dump <| cast "🎉🤣👍🍺"
// => "F0 9F 8E 89 F0 9F A4 A3 F0 9F 91 8D F0 9F 8D BA": ScalarStringshow <| quote "A\nB"
// => "\"A\\nB\"": ScalarStringshow <| single-quote '\n'
// => "'\\n'": ScalarString
show <| sep_by ", " <| map single-quote <| "🎉🤣👍🍺"
// => "'🎉', '🤣', '👍', '🍺'": ScalarStringshow <| prefix "@"
<| bracket
<| sep_by ", "
<| map hex
<| (cast "🎉"):@[u8]
// => "@[0xF0u8, 0x9Fu8, 0x8Eu8, 0x89u8]": ScalarStringshow <| prefix "@"
<| bracket
<| sep_by ", "
<| map (hex << @{Cast a u32}.cast)
<| "🎉🤣"
// => "@[0x1F389u32, 0x1F923u32]": ScalarStringlet id = λx. x;
id 42
// => 42: Int// recursive function version.
let rec fact = λn.
if (0 == n) 1 else n * fact (n - 1);
fact 5
// => 120: Int// iterator pipeline version.
let fact = λn.
counter 1 |> take n |> fold (*) 1;
fact 5
// => 120: Inttype Option a = Some a | None;
let getOrZero = λopt.
match (opt) {
Some x => x,
None => 0
};
getOrZero (Some 42)
// => 42: Inttype Result e a = Ok a | Err e;
let unwrapOr = λr. λdefault.
match (r) {
Ok x => x,
Err _ => default
};
unwrapOr (Err ()) 0
// => 0: Int👉 More examples (with Japanese explanations) are available in examples/README_ja.md.
⚠️ Work in progress — Phox is under active development.
Clone this repository and build with Rust (tested on 1.80+, may work on earlier versions):
cargo buildIf you run without arguments, Phox starts an interactive REPL:
cargo run
> let rec fact = λn. if (0 == n) 1 else n * fact (n - 1);
> fact 5
=> 120: IntIn REPL, an input starts with : is recognized as a REPL command.
For example, :? shows the list of available commands:
cargo run
> :?
:quit, :q
exit REPL.
:help, :h, or :?
print this help messages.
:load <path>, :l <path>
load and evaluate Phox source file specified by <path>.
Pass a .phx file to execute it:
.phxis the conventional extension for Phox source files (plain text)..txtfiles are also accepted.
cargo run examples/fact.phx
=> 120: IntYou can also pipe code from stdin (use - explicitly):
echo "1 + 2" | cargo run -
=> 3: IntResulting value and inferred type are printed on success, like this:
=> value: typeOn error, an error message is printed, like this:
parse error: UnrecognizedToken { /* snip... */ }Example programs are available in the examples/ directory.
- REPL with type inference output
- Standard library (see
assets/directory) - Trait system (multi-parameter type classes)
- Module system
- Function template
*let -
Row polymorphism -
Nat kind (type-level natural numbers)
- Procedures with side-effects
- Dynamic arrays (mutable / growable arrays)
- Unboxed arrays
- Alias analysis and reuse analysis of heap memory.
- Constraint-based multi-parameter type classes (
trait/impl) - Automatic requirements inference for
impls - Higher order trait-record inference (e.g.
@{Iter s a})
- Trait record
-
Split/Merge operators -
Row polymorphism
MIT License