{"size": 4663, "ext": "scrbl", "max_stars_repo_path": "cur-doc/cur/scribblings/curnel.scrbl", "max_stars_repo_name": "jsmaniac/cur", "max_stars_repo_stars_event_min_datetime": null, "max_stars_repo_stars_event_max_datetime": null, "max_issues_repo_path": "cur-doc/cur/scribblings/curnel.scrbl", "max_issues_repo_name": "jsmaniac/cur", "max_issues_repo_issues_event_min_datetime": null, "max_issues_repo_issues_event_max_datetime": null, "max_forks_repo_path": "cur-doc/cur/scribblings/curnel.scrbl", "max_forks_repo_name": "jsmaniac/cur", "max_forks_repo_forks_event_min_datetime": "2021-10-02T16:05:54.000Z", "max_forks_repo_forks_event_max_datetime": "2021-10-02T16:05:54.000Z"}
{"max_stars_count": null, "max_issues_count": null, "max_forks_count": 1, "avg_line_length": 34.2867647059, "max_line_length": 99, "alphanum_fraction": 0.6174136822}
#lang scribble/manual

@(require
  "defs.rkt"
  scribble/eval)

@title{Curnel Forms}
@deftech{Curnel forms} are the core forms provided @racketmodname[cur].
These forms come directly from the trusted core and are all that remain after macro expansion.
@todo{Link to guide regarding macro expansion}
The core of @racketmodname[cur] is essentially TT with an impredicative universe @racket[(Type 0)].
For a very understandable in-depth look at TT, see chapter 2 of
@hyperlink["https://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf"
           "Practical Implementation of a Dependently Typed Functional Programming Language"], by
Edwin C. Brady.

@(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/bool cur/stdlib/prop)"))

@defform*[((Type n)
           Type)]{
Define the universe of types at level @racket[n], where @racket[n] is any natural number.
@racket[Type] is a synonym for @racket[(Type 0)]. Cur is impredicative
in @racket[(Type 0)], although this is likely to change to a more
restricted impredicative universe.

@examples[#:eval curnel-eval
          (Type 0)]

@examples[#:eval curnel-eval
          (Type 1)]

@examples[#:eval curnel-eval
          Type]
}

@defform[(λ (id : type-expr) body-expr)]{
Produces a single-arity procedure, binding the identifier @racket[id] of type
@racket[type-expr] in @racket[body-expr] and in the type of @racket[body-expr].
Both @racket[type-expr] and @racket[body-expr] can contain non-curnel forms,
such as macros.

Currently, Cur will return the underlying representation of a procedure when a
@racket[λ] is evaluated at the top-level.
Do not rely on this representation.

@examples[#:eval curnel-eval
          (λ (x : Type) x)]

@examples[#:eval curnel-eval
          (λ (x : Type) (λ (y : x) y))]


@defform[(#%app procedure argument)]{
Applies the single-arity @racket[procedure] to @racket[argument].
}

@examples[#:eval curnel-eval
          ((λ (x : (Type 1)) x) Type)]

@examples[#:eval curnel-eval
          (#%app (λ (x : (Type 1)) x) Type)]
}

@defform[(Π (id : type-expr) body-expr)]{
Produces a dependent function type, binding the identifier @racket[id] of type
@racket[type-expr] in @racket[body-expr].


@examples[#:eval curnel-eval
          (Π (x : Type) Type)]

@examples[#:eval curnel-eval
          (λ (x : (Π (x : (Type 1)) Type))
            (x Type))]
}

@defform[(data id : type-expr (id* : type-expr*) ...)]{
Defines an inductive datatype named @racket[id] of type @racket[type-expr], with constructors
@racket[id*] each with the corresponding type @racket[type-expr*].
Currently, Cur does not attempt to ensure the well-foundedness of the inductive definition.
For instance, Cur does not currently perform strict positivity checking.

@examples[#:eval curnel-eval
          (data Bool : Type
                (true : Bool)
                (false : Bool))
          ((λ (x : Bool) x) true)
          (data False : Type)
          (data And : (Π (A : Type) (Π (B : Type) Type))
            (conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) ((And A) B)))))))
          ((((conj Bool) Bool) true) false)]
}

@defform[(elim inductive-type motive (index ...) (method ...) disc)]{
Fold over the term @racket[disc] of the inductively defined type @racket[inductive-type].
The @racket[motive] is a function that expects the indices of the inductive
type and a term of the inductive type and produces the type that this
fold returns.
The type of @racket[disc] is @racket[(inductive-type index ...)].
@racket[elim] takes one method for each constructor of @racket[inductive-type].
Each @racket[method] expects the arguments for its corresponding constructor,
and the inductive hypotheses generated by recursively eliminating all recursive
arguments of the constructor.

The following example runs @racket[(sub1 (s z))].

@examples[#:eval curnel-eval
          (data Nat : Type
            (z : Nat)
            (s : (Π (n : Nat) Nat)))
          (elim Nat (λ (x : Nat) Nat)
                ()
                (z
                 (λ (n : Nat) (λ (IH : Nat) n)))
                (s z))]
}

@defform[(define id expr)]{
Binds @racket[id] to the result of @racket[expr].

@examples[#:eval curnel-eval
          (data Nat : Type
            (z : Nat)
            (s : (Π (n : Nat) Nat)))
          (define sub1 (λ (n : Nat)
                         (elim Nat (λ (x : Nat) Nat)
                               ()
                               (z
                                (λ (n : Nat) (λ (IH : Nat) n)))
                               n)))
          (sub1 (s (s z)))
          (sub1 (s z))
          (sub1 z)]
}
@todo{Document @racket[require] and @racket[provide]}
