[[
wikihub
]]
Search
⌘K
Explore
People
For Agents
Sign in
Explore
People
For Agents
Sign in
@jemoka / Jemoka Knowledge Base / raw/concept/kbhtyping.md
Suggest edit
Cancel
Submit suggestion
Title
Name
Note
--- title: "typing" source: https://www.jemoka.com/posts/kbhtyping/ --- what is a type? a type is a set of values. consider List[Int]; importantly, List is not a type; its a “type constructor” which takes a type as input (Int) and gives you as type as output List[int]. -> is another “type constructor”; its a type constructor written in infix notation. It takes two arguments, it constructs a type for set of functions which takes an integer as input and maps it to another integer Int -> Int types are rules of inference “If Hypothesis is true, then Conclusion is true” “If E1 and E2 have certain types, then E3 has a certain type” For instance: if \(e_1\) has type Int and \(e_2\) has type Int, then \(e_1 + e_2\) has type Int. inference rule notation \begin{equation} \frac{\vdash H_{1} \dots \vdash H_{n}}{\vdash C} \end{equation} where each \(H_{j}, C\) have the shape \(\vdash e: T\), that some \(e\) has type some \(T\) summation \begin{equation} \frac{\vdash e_1 : Int, \vdash e_2: Int}{\vdash e_1+e_2 : Int} \end{equation} combining rules suppose you need to first show that \(1\) and \(2\) are integers \begin{equation} \frac{\frac{\vdash 1: \text{1 is an integer}}{\vdash 1 : Int}, \frac{\vdash 2: \text{1 is an integer}}{\vdash 2 : Int}}{\vdash 1+2 : Int} \end{equation} type rules variables \begin{equation} \frac{}{A, x: t \vdash x: t} \end{equation} if you assume \(x:t\), then \(x:t\) integers \begin{equation} \frac{}{A \vdash i: int} \end{equation} we call \(i\) any int function applications \begin{equation} \frac{\begin{align} &A \vdash e_1: t \to t’\\ &A \vdash e_2 : t \end{align}}{A \vdash e_1e_2: t’} \end{equation} if my function \(f\) takes \(t\) to \(t’\), then applying it to a \(t\) will give you a \(t’\) abstraction \begin{equation} \frac{A, x:t \vdash e: t’}{A \vdash \lambda x:t . e : t \to t’} \end{equation} if we can prove that with a thing \(x\) of type \(t\) we can force \(e\) to be type \(t’\), then the lambda wrapped around it would have the signature \(t \to t’\). let \begin{equation} \frac{\begin{align} &A \vdash \lambda x.e : t, A \\ &f: t \vdash e’ : t' \end{align}}{A \vdash let\ f=\lambda x.e \text{ in } e’ : t’} \end{equation} environment Environments gives types for free variables—an environment is a function from variables to types. Let \(A\) be a function from free variables to type. For instance, \(A \vdash e:T\), meaning “under the assumption that variables have types by \(A\), its provable that the expression \(e\) has type \(T\). We have then tack on this on \begin{equation} \frac{A \vdash e_1 : Int, A \vdash e_2: Int}{A\vdash e_1+e_2 : Int} \end{equation} variables \begin{equation} \frac{A(x) = T}{A \vdash x:T} \end{equation} religion For a type system that doesn’t allow primitive recursion, there maybe type duplication because you can’t assign a thing into multiple types. type inference see type inference for every new application, we wrote \begin{equation} \frac{A \vdash f: t \to t’, A \vdash e : t}{A \vdash f e: t’} \end{equation} now, we modify this with a new type variables \begin{equation} \frac{t=t’ \to \beta, A \vdash e_1: t, A \vdash e_2 : t’}{A \vdash e_1e_2: \beta} \end{equation} and now, to actually type things, we just want to solve for \(\beta\). we then solve the constraints: S, t = ⍺ => S, t = ⍺, ⍺ = t [Symmetry] S, ⍺ = t1, ⍺ = t2 => S, ⍺ = t1, ⍺ = t2, t1 = t2 [Transitivity] S, t1 → t2 = t3 → t4 => S, t1 → t2 = t3 → t4, t1 = t3, t2 = t4 [Structure] infiite solutions Consider: \begin{equation} x = int \to x \end{equation} constraint solving for each equation \(A=B \in S\), check that \(A’ = C(\emptyset, S, A)\) is defined canonicalization