Title: Theory / Unimportant / CS / Programming / LISP / Little / Typer+15
Tags: declaration todo_declaration

Name: A form a judgement
Definition: An observation with blank spaces in it, such as ___is a ___
Page: 5
Chapter: 1
Context: type

Name: The second form a judgement
Definition: ___ is the same ___ as ___
Page: 5
Chapter: 1
Context: type
Example: 'citron is the same Atom as 'citron

Name: The third form a judgement
Definition: ___ is a type
Page: 8
Chapter: 1
Context: type
Example: (Pair Atom Atom) is a type

Name: The fourth form a judgement
Definition: ___ and ___ are the same type
Page: 8
Chapter: 1
Context: type

Name: An ill-typed expression
Definition: An expression that can not be described by a type and is not a type
Page: 14
Chapter: 1
Context: type

Name: Normal form of an expression
Definition: the most direct way of writing the expression
Page: 12
Chapter: 1
Context: type

Name: Cons expressions which are the same
Definition: Cons-expressions with the same car and the same cdr
Page: 14
Chapter: 1
Context: type

Instruction: (claim varName type)
Page: 20
Effect: Ensure that the variable varName has type
Context: lisp typing
Chapter: 1

Name: A normal expression
Definition: A constructor applied to normal expressions (potentially zero)
Page: 21
Chapter: 1
Context: lisp typing

Name: A value
Definition: An expression with a constructor at the top
Page: 21
Chapter: 1
Context: lisp typing

Name: The top of an expression
Definition: The first element occurring in the expression
Page: 21
Chapter: 1
Context: lisp typing

Name: Two values are the same
Definition: The values have the same constructor
Page: 21
Chapter: 1
Definition2: the values have constructor arguments that are pairwise the same

Name: Two expressions that are the same
Definition: Two expressions whose values are the same
Page: 27
Chapter: 1

Name: A type constructor
Definition: An expression that, when given type argument, create a type
Page: 30
Chapter: 1
Example: Pair

Name: A constructor
Definition: An expression that, when given expressions arguments (potentially 0), create a type
Page: 30
Chapter: 1
Example: cons

Name: An eliminator
Definition: An expression that takes a values created by a constructor and takes its values
Page: 33
Chapter: 2
Example: car cdr
Example2: applyng a function to arguments

Typ: (-> foo_1 ... foo_n bar)
Meaning: Type of function taking a foo_1 ... foo_n as arguments and returing a bar
Page: 36
Chapter: 2

Name: Lambdas expression that are the same
Definition: whose bodies are the same (up to consistent renaming)
Page: 37
Chapter: 2
Definition2: take the same number of argument
Conjdef: with
DefType: Lambda expressions

Smaller0: an \(-> Y X\)
Greater0: \(X\)
Page: 38
Chapter: 2
Prefix Greater: \((f arg)\)
Smaller1: a \(Y\)
Name: Initial law of application
Prefix Smaller: \(f\) is
Connect Smaller0: , \(arg\) is

Name: Initial second commandment of \(\lambda\)
Definition: \(f\) is the same as \(\lambda (y) (f y)\) for \(y\) not in \(f\)'s body
Page: 38
Chapter: 2
Variables: f: (-> Y X)

Name: The law of renaming variables
Definition: Consistently renaming variables can’t change the meaning of anything
Page: 39
Chapter: 2

Name: A neutral expression
Definition: An expression that is not a value and cannot yet be evaluated due to a variable
Page: 40
Chapter: 2
Example: (car x)
Example2: f zero

Name: Neutral expressions which are the same
Definition: Expressions with identical eliminators at the top top and all arguments to the eliminators are the same
Page: 41
Chapter: 2

Instruction: (define varName expr)
Page: 43
Meaning: Introduce varName as a constant whose value is the evaluation of expr
Chapter: 2
Assuming: all names in expr are already defined. In particular it does not conatins varName

Smaller0: (claim name X)
Greater0: name is an X
Page: 43
Chapter: 2
Smaller1: (define name expr)
Name: The Law and Commandment of define
Greater1: name is the same X as expr
Smaller2: expr is an X

Smaller0: a (Pair A D)
Page: 44
Chapter: 2
Prefix Greater: p is the same as
Name: The Second Commandment of cons
Connect Greater0: (cons (car p) (cdr p))
Prefix Smaller: p is

Question: Examples of expressions which are the same only for certain type
Answer: (cons (car p)(cdr p)) is the same as p iff p is a Pair
Page: 44
Chapter: 2

Instruction: (which-Type expr
  constr_1_case
  ...
  const_n_case)
Page: 45
Chapter: 2
Returns: If expr 's constructor is constr_i and the arguments are arg_1, ..., arg_m, then (constr_i_case arg_1 ... arg_m)
Assuming: constr_i_case : i-th constructor args -> return_type
Typ: return_type

Name: Universe
Definition: The smallest set closed under type constructor
Page: 53
Chapter: 2
Notation: \(\mathcal U\)

Name: Pie
Definition: Language, variant of lisp, used in The little typer
Page: 63
Chapter: 3

Instruction: (the type value)
Page: 64
Effect: fail if value's type is not type
Chapter: 3
Returns: value

Name: A total function
Definition: A function that always assigns a value to every possible argument
Page: 71
Chapter: 3

Instruction: \(\prod ((A_1 U_1) ... (A_n U_n)) \) Body_Type
Page: 99
Chapter: 4
Returns: A function that takes type variables A_i belonging to U_i return Body_Type
Name: A Pi expression

Typ: (List E)
TypMeaning: List whose all elements are E
Page: 110
Chapter: 5
Value: nil: empty list
Value2: (cons e l) with e:E and l: (List E)