Topaz is a programming language created in 2021 by m-schm.
| #2207on PLDB | 3Years Old |
git clone https://github.com/m-schm/topazDependently typed language that compiles to JavaScript
;; A comment
;; `Ven n a` represents lists that are `n` long, that contain `a`s
;; A Vec is either:
type Vec (n: Uint) (a: Type) =
;; empty, with length 0...
Nil: {a} -> Vec 0 a
;; or 1 item longer than a Vec of length n.
`::`: {n a} -> a -> Vec n a -> Vec (n+1) a
;; `zip` should take two lists and return a list of pairs.
;; The two lists are required to be the same length because `n` is the same for
;; both parameters.
let zip {n a b} (left: Vec n a) (right: Vec n b): Vec n (a, b) =
match left, right in
;; Either both lists are empty...
Nil, Nil => Nil
;; or they both contain at least one item.
x :: xs, y :: ys => (x, y) :: zip xs ys
;; No other cases are needed, because the lists are the same length!