language.txt

-- What works now as of June 1, 2025.

-- Comments start with -- and go until the end of line.

-- Any combination of +-*/<>=:%^&|!~$?# is an operator.
-- But these are part of language syntax: | => -> = :

-- Identifiers start with a lowercase letter and then may have
-- letter, digits, _ and ?.

-- Type names and data constructors start with an uppercase letter
-- and then may have letters, digits and _.

aFloat = 1.23
anInt = 23
aString = "hey"
aChar = 'a'        -- ''' is the char of the single quote
o_o? = False

-- A program consists of top level items like
-- type / type class / instance / function / variable definitions, and expressions.

-- Function / variable definitions may start with a type signature:
-- name : type scheme
-- then one or more lines with equations like 'name [patterns] = expr'

or : Bool -> Bool -> Bool
or True _ = True
or _    x = x

aBool = or False True

mustBe expected actual =
  if actual == expected then puts "ok "
  else puts("Oops! " ~ show actual ~ " is not the expected " ~ show expected ~ "\n")

-- top level expressions get evaluated one by one
-- x ^ f === f x, so  x ^ f y === f y x
aBool ^ mustBe True

-- Predicates about type classes are given after `where` in a poly type.
println : a -> () where Show a
println x = do
  puts (show x)
  puts "\n"

-- Block expressions start with `do` and use off-side rule, where indentation shows where it ends.
-- { } can also be used explicitly. `;` can separate expressions on same line

greet : String -> ()
greet x = do { puts "hi "; println x }

greet2 x = { puts "Hey "; println x }   -- `do` before {...} is optional

greet "Joe"
greet2 "Jack"

-- Lambdas: { arg1 arg2 ... => exprs }

twice = { x f => f x; f x }

twice "pe" { a =>
  puts "well "
  greet (a ~ a)
}

-- Match: match arg1 arg2 ... { | pat1 pat2 ... => expr | ... }

m1 = match 1 "Ok" True {
  | 0 "qq" False => "0"
  | 1 s    _     => s
}

m1 ^mustBe "Ok"

-- Without args match becomes a function:

cal = match { | a "+" b => a + b
              | a "-" b => a - b }

cal 2 "+" 3   ^mustBe 5
cal 9 "-" 2   ^mustBe 7


-- Algebraic types:
type Vec = Vec2 { x : Int; y : Int } | Vec3 { x:Int; y:Int; z:Int}

-- `Vec` is the type name, `Vec2` and `Vec3` are tags for structs.
-- An algebraic type contains 1 or more tagged structs.
-- Each struct has 0 or more named fields.

showVec : Vec -> String
showVec (Vec2 x y)   = "Vec2 " ~ show x ~ " " ~ show y
showVec (Vec3 x y z) = "Vec3 " ~ show x ~ " " ~ show y ~ " " ~ show z

showVec (Vec2 3 4)   ^mustBe "Vec2 3 4"
showVec (Vec3 4 5 6) ^mustBe "Vec3 4 5 6"

-- Patterns for structs can also be Tag { fldName: pat; fldName: pat ...}
-- Don't have to mention the fields you don't need.

sumXY Vec2 {x:xx; y:yy} = xx + yy
sumXY Vec3 {x:xx; y:yy} = xx + yy

sumXY (Vec3 30 40 50)   ^mustBe 70

-- Another pattern variant for structs: `Tag:var`
-- Struct fields can be accessed using `.name`.

addVecs Vec2:a  Vec2:b  = Vec2 {x: a.x + b.x; y: a.y + b.y}
addVecs Vec3:a  Vec3:b  = Vec3 (a.x + b.x) (a.y + b.y) (a.z + b.z)

addVecs (Vec2 10 20)    Vec2{x: 100; y: 200}         ^ showVec ^ mustBe "Vec2 110 220"
addVecs (Vec3 10 20 30) Vec3{x: 100; y: 200; z: 300} ^ showVec ^ mustBe "Vec3 110 220 330"

getZ v = v.z     -- type inferred as Vec3 -> Int, since only Vec3 has field z

-- getX v = v.x  -- this will not compile without a type annotation, as field x is not unique.

getZ (Vec3 4 5 6) ^mustBe 6


-- Algebraic types allow subtraction of components, using `- Tag`.
type V2 = Vec - Vec3
-- V2 only contains Vec2 structs now

justXY : Vec -> V2
justXY Vec2:v = v                 -- same value, no conversion required
justXY Vec3:v = Vec2 v.x v.y

-- Values of V2 also belong to Vec, so showVec works. V2 is a subtype of Vec!
Vec2 11 12    ^ justXY ^ showVec ^ mustBe "Vec2 11 12"
Vec3 31 32 33 ^ justXY ^ showVec ^ mustBe "Vec2 31 32"


-- We can also extend algebraic types by adding more components:
type VecOrScalar = Vec | Sca { x: Int }

-- VecOrScalar contains structs Vec2, Vec3, and Sca.

showVecOrScalar : VecOrScalar -> String
showVecOrScalar (Sca x) = "Sca " ~ show x
showVecOrScalar Vec2:v = showVec v
showVecOrScalar Vec3:v = showVec v

showVecOrScalar (Sca 99) ^mustBe "Sca 99"

v3 : Vec
v3 = Vec3 1 2 3

v2 : V2
v2 = justXY v3

-- showVecOrScalar can accept not just VecOrScalar but also all its subtypes like Vec and V2
showVecOrScalar v3 ^mustBe "Vec3 1 2 3"
showVecOrScalar v2 ^mustBe "Vec2 1 2"


-- Generic types
type GenObj t = G {
  val     : t
  printer : t -> ()
}

printGenObj a = a.printer a.val

sv : GenObj Vec
sv = G { val: Vec2 11 12;   printer: {v => showVec v ^ println }}

ss : GenObj String
ss = G { val: "str\n";      printer: puts }

printGenObj sv
printGenObj ss

-- Types with a single struct (i.e. not a sum) where struct name is the same as type name
-- can be defined using a shorter syntax:

type MyStruct a b {
  aa : a
  bb : b
  cc : Int
}

(MyStruct 1 True 2).aa ^mustBe 1

-- Type classes:

class Named nt {
  typeName : nt -> String

  -- method signatures may have their own predicates too
  seri : nt -> String where Show nt
}

instance Named String { typeName x = "String"; seri x = "S " ~ x }
instance Named Bool   { typeName x = "Bool"  ; seri b = "B " ~ show b }

instance Show (GenObj a) where Show a {  -- instance predicate
  show g = show g.val
}

instance Named (GenObj a)  where Named a {
  typeName g = "Gen " ~ typeName g.val
  seri     g = "G " ~ seri g.val
}

nameIt x = typeName x ~ "!"

typeName (G "qq" puts) ~ ", " ~ nameIt (G True {_ => ()})  ^mustBe "Gen String, Gen Bool!"

seri True          ^mustBe "B True"
seri (G "ee" puts) ^mustBe "G S ee"

instance Show Vec { show = showVec }

-- Superclasses - class predicates:

class NamedTwice t where Named t {
  dname : t -> String
}

instance NamedTwice Bool { dname x = {s = typeName x; s~s} }

nameThrice x = dname x ~ typeName x      -- inferred type: ∀ x . NamedTwice x => (x) -> String

nameThrice True ^mustBe "BoolBoolBool"


-- Multiparameter type classes

class VecSpace v s {
  mul : v -> s -> v
}

instance VecSpace Vec Int {
  mul (Vec2 x y)   k = Vec2 (x*k) (y*k)
  mul (Vec3 x y z) k = Vec3 (x*k) (y*k) (z*k)
}

mul      (Vec3 1 2 3) 10  ^show ^mustBe "Vec3 10 20 30"
mul      (Vec2 1 2)   10  ^show ^mustBe "Vec2 10 20"


-- Arrays:
id x = x
a = id [1, 2, 3]   -- If there's some whitespace before [, it's an array literal.
a[1] ^mustBe 2     -- Without whitespace, it's an indexing operation.
                   -- Currently arrays are immutable and covariant.

-- Functional dependencies in MPTC:
-- this definition mirrors OpIndex defined in the prelude

class MyOpIndex c e | c -> e {   -- here the type e will be dictated by c
  myopIndex : c -> Int -> e
}

-- A shorter syntax for the same:
class MyOpIndex2 c -> e {
  myopIndex2 : c -> Int -> e
}

instance MyOpIndex (Array t) t {
  myopIndex a i = a[i]
}

arr = [1,2,3]
aa = [arr, arr]

myopIndex (myopIndex aa 1) 2 ^mustBe 3

-- Mutable fields in structs:
type MS = MS { mut a : Int; mut b : Int; c : Int }
o = MS 1 2 3
o.b := 4               -- set one field
o.a ^mustBe 1
o.b ^mustBe 4

o := {b: 20; a: 10}    -- set multiple fields

o.a ^mustBe 10
o.b ^mustBe 20
o.c ^mustBe 3