The Carth Reference

This document is the primary reference for the Carth programming language. It is updated on a best-effort basis. It should be valid and complete, but it may not be.

1 TODO Introduction

1.1 TODO How to use this document

1.3 TODO Influences

1.4 TODO Glossary

2 TODO Lexical structure

For details about the syntax that are not covered explicitly in this document or cannot be inferred from the provided examples, please consult the source of the parser directly in Parse.hs.

3 TODO Macros

4 TODO Packages, modules, and source files

5 TODO Items

5.1 Global variable definitions

Global variables are defined at the top-level by using either one of the two implicitly typed variable define and function define special forms, or their explicitly typed define: counterparts.

Global variables are practically equivalent to local variables, in all respects but scope.

5.1.1 Examples

;; First form. Implicitly typed variable definition.
;; Bind the global variable ~id-iv~ to the identity function. No explicit type
;; signature is given - it is statically inferred by the typechecker to be the
;; equivalent of ~(forall [a] (Fun a a))~
(define id-iv
  (fun x x))

;; Second form. Implicitly typed function definition.
;; Again, the identity function, equivalent to the defition above, but using the
;; more convenient function definition syntax.
(define (id-if x)

;; Third form. Explicitly typed variable definition.
;; Explicit type signature is given. The type must properly be a polytype (aka
;; /type scheme/) to be valid and instantiable for any monotype.
(define: id-ev
    (forall [a] (Fun a a))
  (fun x x))

;; Fourth form. Explicitly typed function definition.
(define: (id-ef x)
    (forall [a] (Fun a a))

5.2 Type definitions

Algebraic datatypes (aka tagged/discriminated unions) are defined at the top-level with the type special form. Roughly equivalent to data in Haskell and enum in Rust.

5.2.1 Examples

;; First form. Monomorphic datatype definition.
;; ~Age~ only has one variant, and as such can be seen as a "wrapper" around
;; ~Int~, restricting its usage.
(type Age

;; Second form. Polymorphic datatype definition.
;; ~List~ has two variants, representing that a list can either be empty, or a
;; pair of a head and a tail.
(type (List a)
  (Cons a (List a)))

6 TODO Expressions

6.1 Literals

unit is the only value inhibiting the type Unit, equivalent to () in Haskell and Rust.
64-bit signed integer literal. Example: 42.
64-bit double precision floating point literal. Example: -13.37.
4-byte UTF-32 Character literal. Example: 'a', '維', '🔥'.
UTF-8 string literals. At the moment, generates to static arrays. Will likely be changed. Example: "Hello, World!", "😄😦🐱".
True or False.

6.2 TODO Variable

6.3 TODO Function application

6.4 TODO Conditional

6.5 TODO Anonymous-function / Lambda expression / Closure

6.6 TODO Let

6.7 Type ascription

Type ascriptions are primarily used to:

  • increase readability when the type of an expression is not obvious;
  • assert at compile-time that an expression is of or can specialize to the given type;
  • or specialize the type of a generic expression, restricting its usage.

6.7.1 Example

(: x Int)

6.8 Match

Pattern matching. Used to deconstruct algebraic datatypes.

Note that the cases of a match-expression must be exhaustive and non-redundant.

6.8.1 Example

CUSTOM_ID: Match-Example
(type Foo
(type (Pair a b)
  (Pair a b))

;; Ok
(define (fst pair)
  (match pair
    [(Pair a _) a]))

;; Error. Redundant pattern. ~Pair _ _~ already covered by previous pattern ~_~
(define (redundant pair)
  (match pair
    [_ 1]
    [(Pair x y) 2]))

;; Error. Inexhaustive pattern. All cases not covered, specifically ~Bar~
(define (inexhaustive foo)
  (match foo
    [Baz 123]))

6.9 FunMatch

Syntax sugar for a match in a lambda. Equivalent to \case (LambdaCase) in Haskell. (fun-match cases...) translates to (fun VAR (match VAR cases...)) where VAR is a uniquely internally generated variable that cannot be expressed by the user (which means it won't shadow any other binding).

6.9.1 Example

;; Two versions of `fst`, which returns the first value of a pair
;; using normal `match`
(define (fst-nofun p)
  (match p
    [(Pair a _) a]))
;; and using `fun-match`
(define fst-fun
    [(Pair a _) a]))

6.10 Constructor

By applying a constructor to some arguments, or just presenting it literally in the case of a nullary constructor, a value of the associated algebraic datatype is produced. Constructors of arity > 0 behave like n-ary functions: curried and the whole shebang.

6.10.1 Example

;; The following datatype definition will make available the constructors ~Unit~
;; and ~Pair~ in the environment.
(type UnitOrPair
  (Pair Int Int))

;; The ~Unit~ constructor is nullary, and will construct a ~UnitOrPair~ just
;; presented literally.
(define: unit

;; The ~Pair~ constructor is binary, and takes two arguments to construct a
;; ~UnitOrPair~. It behaves like a function of two ~Int~ arguments, returning a
;; ~UnitOrPair~.
(define: pair''
    (Fun Int Int UnitOrPair)
(define: pair'
    (Fun Int UnitOrPair)
  (Pair 3))
(define: pair
  (pair' 5))

7 Patterns

Patterns are used to conditionally deconstruct values of algebraic datatypes in pattern-matching contexts.

There are 3 kinds of patterns: nullary constructors, n-ary constructions, and variable bindings.

7.1 Example

8 TODO Type system

9 TODO Memory model

10 TODO Linkage

11 TODO Unsafety

12 TODO Compile time evaluation

13 TODO Runtime

14 TODO Literate Carth

CUSTOM_ID: Literate-Carth

Carth has native support for literate programming with Org mode. Either use Emacs with Babel in Org-mode for an interactive session, or interpret/compile the file with carth just like a normal .carth file!

14.1 Example

Consider a file with the following content:

#+TITLE: Literate Programming Rules!

Literate programming is just really cool!

~carth~ will assume ~tangle~ = ~yes~ by default, but setting it
explicitly won't hurt.

#+BEGIN_SRC carth :tangle yes
(define (main _)
  (printInt (id 1337)))

* The ~id~ function
  ~id~ is the identity function. It returns its argument unchanged.

  #+BEGIN_SRC carth
  (define (id x) x)

* How not to use ~id~
  Here is an example of how not to use ~id~. Note that this won't
  compile. We show this in a SRC block to get syntax highlighting etc,
  but as ~tangle~ is ~no~, this source block will be ignored by carth.

  #+BEGIN_SRC carth :tangle no
  (printInt id)

When e.g. interpreting this file with carth i, the Carth source will untangled from the rest of the document. Line numbers are preserved. The result of the untangling stage will be the following:

(define (main _)
  (printInt (id 1337)))

(define (id x) x)

And for completeness, the result of interpreting that will be 1337.