Bindings

Contents

Items

Let bindings are made up of items. At the moment these can either be declarations or definitions.

A declaration states the type for of an identifier that we should expect to see in a subsequent definition for that identifier. For example:

let
    greeting : String;              -- declaration
    greeting = "hello there!";      -- definition
in
    ...

We can make supply a number of forward declarations before providing their associated definitions:

let
    one : S32;
    two : S32;

    one = 1;
    two = 2;
in
    ...

Values that can be inferred do not require a declaration, although sometimes a declaration may be useful for documentations purposes!

let
    string = "hello"  -- ok!
    one = 1 : U16     -- ok!
    two = 2           -- error: is this an U8, U16, S64, etc?
in
    ...

Function definitions

We have some nice syntactic sugar for defining functions. For example:

let
    const : (a b : Type) -> a -> b -> a;
    const = \a b x y => x;
in
    const String I32 "hello" 1

Could be expressed more cleanly as:

let
    const : (a b : Type) -> a -> b -> a;
    const a b x y = x;
in
    const String I32 "hello" 1

Type aliases

Because Pikelet is dependently typed, we need no other mechanism for making type aliases. Instead we just use definitions!

let
    Name : Type;
    Name = String;

    bobs-name : Name
    bobs-name = "bob"
in
    ...

Doc comments

Documentation can be provided for above declarations, by using doc comments:

let
    ||| This is a documented definition
    |||
    ||| # Example
    |||
    ||| ```pikelet-repl
    ||| Pikelet> self-aware-string
    ||| "I am a string!" : String
    ||| ```
    self-aware-string : String;
    self-aware-string = "I am a string!";
in
    ...