FR
PréludeChargé par défaut — aucun import nécessaire.

Core data types

Synopsis 
data Unit = Unit

Unit has exactly one value: Unit, also written ().

data Bool = True | False

Bool has two values. Used by if-then-else and guards.

data Nat
  = Z
  | S Nat

Nat is the type of natural numbers (0, 1, 2, ...). Internally backed by arbitrary-precision integers, not Peano.

Z

zero

S

the successor of a natural (S n = n + 1)

data String
  = Empty
  | Cons Char String

String is a text, stored packed (UTF-8), not built from cells. These two constructors are its VIEW: a string is Empty, or Cons c s — its first character c followed by the rest s — in a pattern as in an expression (Cons 'a' "bc" is "abc"). Like Nat, the compiler keeps the native form.

Empty

the empty string, also written ""

Cons

a first character in front of the rest

data Pair a b = Pair a b

Pair groups two values. Written (a, b) via notation below.

data Maybe a
  = Nothing
  | Just a

Maybe represents optional values: Nothing or Just x.

Nothing

no value

Just

a value, wrapped

data Either a b
  = Left a
  | Right b

Either represents a choice between two types.

Left

by convention, the error case

by convention, the success case

data Result e a
  = Ok a
  | Error e

Result represents an operation that can fail: Ok x carries a success value, Error e carries an error. Unlike Either, the constructor names say which side is which (as in OCaml/F#/Gleam). The error type comes first so that map-like operations work on the success value (the last parameter).

Ok

success, carrying a value

Error

failure, carrying an error

data List a
  = Nil
  | a :: List a

List is the fundamental recursive data structure.

Nil

the empty list, also written []

::

a head element in front of a tail list (infix, like Haskell's :)