reference.org 8.09 KB
Newer Older
JoJo's avatar
JoJo committed
1 2 3 4 5 6 7 8 9 10 11
#+TITLE: The Carth Reference
#+INCLUDE: "../page.org"

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.

* TODO Introduction
** TODO How to use this document

** TODO Contributing
12
   [[https://gitlab.com/JoJoZ/carth-website/tree/master/pages/reference.org][Here is this file in the gitlab repository]].
JoJo's avatar
JoJo committed
13 14 15 16 17 18

** TODO Influences

** TODO Glossary

* TODO Lexical structure
19 20 21
  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 [[https://gitlab.com/JoJoZ/carth/blob/master/src/Parse.hs][Parse.hs]].
JoJo's avatar
JoJo committed
22 23 24 25 26 27

* TODO Macros

* TODO Packages, modules, and source files

* TODO Items
28
** Global variable definitions
29 30 31 32 33 34 35 36 37 38 39 40
   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.

*** Examples
    #+BEGIN_SRC carth
    ;; First form. Implicitly typed variable definition.
    ;;
41
    ;; Bind the global variable ~id-iv~ to the identity function. No explicit type
42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66
    ;; 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)
      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))
      x)
    #+END_SRC
JoJo's avatar
JoJo committed
67

68 69 70 71
** 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.
JoJo's avatar
JoJo committed
72

73 74 75 76 77 78 79 80
*** Examples
    #+BEGIN_SRC carth
    ;; 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
      Int)
JoJo's avatar
JoJo committed
81

82 83 84 85 86 87 88 89
    ;; 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)
      Nil
      (Cons a (List a)))
    #+END_SRC
JoJo's avatar
JoJo committed
90

91 92 93 94 95 96 97 98 99 100 101
* TODO Expressions
** Literals
- Unit :: ~unit~ is the only value inhibiting the type ~Unit~,
          equivalent to ~()~ in Haskell and Rust.

- Int :: 64-bit signed integer literal. Example: ~42~.
- Double :: 64-bit double precision floating point literal. Example: ~-13.37~.
- Char :: 4-byte UTF-32 Character literal. Example: ~'a'~, ~'維'~, ~'🔥'~.
- String :: UTF-8 string literals. At the moment, generates to static
            arrays. Will likely be changed. Example: ~"Hello, World!"~, ~"😄😦🐱"~.
- Bool :: ~True~ or ~False~.
JoJo's avatar
JoJo committed
102 103 104 105 106 107 108 109 110 111
** TODO Variable

** TODO Function application

** TODO Conditional

** TODO Anonymous-function / Lambda expression / Closure

** TODO Let

JoJo's avatar
JoJo committed
112
** Type ascription
JoJo's avatar
JoJo committed
113 114 115 116 117 118
   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.

*** Example
119
    #+BEGIN_SRC carth
JoJo's avatar
JoJo committed
120 121 122
    (: x Int)
    #+END_SRC

123 124 125
** Match
   Pattern matching. Used to deconstruct algebraic datatypes.

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

129
*** Example
130 131 132
    :PROPERTIES:
    :CUSTOM_ID: Match-Example
    :END:
133
    #+BEGIN_SRC carth
134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154
    (type Foo
      Bar
      Baz)
    (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]))
155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176
    #+END_SRC

** 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).

*** Example
    #+BEGIN_SRC carth
    ;; 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
      (fun-match
        [(Pair a _) a]))
    #+END_SRC
JoJo's avatar
JoJo committed
177

178 179 180 181 182
** 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.
JoJo's avatar
JoJo committed
183

184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220
*** Example
    #+BEGIN_SRC carth
    ;; The following datatype definition will make available the constructors ~Unit~
    ;; and ~Pair~ in the environment.
    (type UnitOrPair
      Unit
      (Pair Int Int))


    ;; The ~Unit~ constructor is nullary, and will construct a ~UnitOrPair~ just
    ;; presented literally.
    (define: unit
        UnitOrPair
      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)
      Pair)
    (define: pair'
        (Fun Int UnitOrPair)
      (Pair 3))
    (define: pair
        UnitOrPair
      (pair' 5))
    #+END_SRC
* 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.

** Example
   See [[#Match-Example][Match/Example]].
JoJo's avatar
JoJo committed
221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313
* TODO Type system

* TODO Memory model

* TODO Linkage

* TODO Unsafety

* TODO Compile time evaluation

* TODO Runtime
* TODO Literate Carth
  :PROPERTIES:
  :CUSTOM_ID: Literate-Carth
  :END:
  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!

** Example
   Consider a file ~cool.org~ with the following content:

   #+BEGIN_SRC org

   ,#+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)))
   ,#+END_SRC

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

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

   ,* 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)
     ,#+END_SRC

   #+END_SRC

   When e.g. interpreting this file with ~carth i cool.org~, 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:

   #+BEGIN_SRC carth









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






   (define (id x) x)











   #+END_SRC

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