$$ \def\por{\ \ | \ \ } \def\dom{\textsf{dom}} \def\tsf#1{\textsf{#1}} \def\unifyj#1#2#3{#1 \sim #2 \Downarrow #3} \def\dict#1#2{\textsf{Dict}\left( #1, #2 \right)} \def\pf{\hookrightarrow}%\rightharpoonup \def\tone{{t_1}} \def\ttwo{{t_2}} \def\rule#1#2#3{\dfrac{#3}{#2}\ {#1}} \def\eqdef{\overset{\textsf{def}}{=}} \def\freevars{\textsf{free}} $$ Unification is probably one of the most important concepts in computer science. If you are not aware, unification is basically the process you undergo to find out how two syntactic objects like $a+b$ and $a+2c$ can be the same thing. In this case, you replace $b$ with $2c$.

$$\def\mathblue#1{\colorbox{blue}{$#1$}} \def\mathgreen#1{\colorbox{green}{$#1$}} \def\mathred#1{\colorbox{red}{$#1$}} \def\mathhl#1{\colorbox{Orchid}{$#1$}} \def\lequiv{\fallingdotseq}$$ $\def\lequiv{\fallingdotseq}$ What mathematics describes is a long standing issue in philosophy. It is hard to break into this subject, but I hope that my intent can be shared. Since I am a mathemtics student who is interested in formal systems, I can’t help to feel nervous when my professor says $A$ is a subset of $B$ if for all $x$, $x\in B$ whenever $x \in A$,

$$\def\infer#1#2{\dfrac{#2}{#1}}$$ Rule systems are seen in almost every programming languages paper. They are a tool for conveying very precise notions of computation. In general, is not easy to give a succinct definition of a rule system, but one can be described easily by adopting a specific representation. A rule system consists of a set of statements of the form $$\infer{Q}{P_1 \quad \ldots \quad P_n}$$ where $Q,P_i$ are propositional schemata. Here, $Q$ is called the conclusion and $P_i$ are called the premises.

Consider the C function int f(int a, int b) { int s = 4; int x,y; x = a * s; s = s + 1; y = b * s; s = s + 1; return x * y; } If we were to write it in Haskell, it would be f :: Int -> Int -> Int f a b = let s = 4 in type Choice a = [a] choose :: [a] -> Choice a choose xs = xs 1

Hello! Hello newtype StateT s m a = StateT { runStateT :: s -> m (a,s) } $$A \to B$$ $$ A $$ $ B $

You should know what sets and types are, what a function is, and the consequences of composing functions. In a programming language, you have types that are given to you and types that you can construct with your own definitions. Some examples of these are Int, Bool, and function types Int -> Int -> Int. You may also may have types that generalize over types, an example is the type Optional<T> where T refers to any type.