First we have the following two examples of recursive functions
func toStrings(L: int list) string list =
case l of
[] => []
| x::xs =>
IntToString(x)::toStrings(xs)
func add(l: int list, a: int) int list =
case l of
[] => []
| x::xs => (a+x)::add(xs,a)
We can have a more general function as the following
map: for all a and b, (a->b)->a list -> b list
fun map f l =
case l of
[] => []
| x::xs => f(x)::map[a][b](xs)
It is called polymorphism generality.
To achieve these, we need variables in type: we have the following judgement
where $\Delta$ means $t_1\ type,…,t_n\ type$
Take the map
function as an example:
It reads as: $(a\rightarrow b)\rightarrow a\ list\rightarrow b\ list$ is a type assuming that $a$ is a type and $b$ is a type.
The inference rule for that
This is a project I did in my undergrad, so I might forget some of the details. Also some of the design choices might seen stupid for now, but I am writing them down anyway just for note-taking. The codes on Github. And here is the presentation we have. I assume the readers of this post have basically knowledge of computer science, like graphs, but not necessarily mathematics (I am really bad at mathematics in fact).
According to Wolfram Research, it is to Find the minimum number of guests that must be invited so that at least m will know each other or at least n will not know each other. The solutions are known as Ramsey numbers. To phrase it in Computer Science word, for $R(n,m)$, it is to find a complete graph with minimum vertices such that if we color edges in two colors, there is no monochromatic n-cliques and m-cliques in any edge labelling. A counter example of $R(n,m)$ is basically a graph with a a labeling that contains monochromatic clique(s).
How hard is this? Well we know that $R(3,3)=6$, $R(4,4)=18$, and we don’t know anything above $R(4,4)$. For $R(10,10)$, the current bounds are $798$ to $23556$. In the project, we are to design an algorithm/system that make use of basically endless computing power from both super-computers (XSEDE, CondorHTC), and cloud platforms (AWS) to find the largest counter example of $R(10,10)$.
In CPython, the global interpreter lock, or GIL is a mutex that prevents multiple threads from executing Python bytecodes at once. The lock is necessary mainly because CPython’s memory management is not thread-safe.
0 import time
1 import threading
2 import multiprocessing
3
4 NUM = 10000000
5
6 def count(n):
7 while n > 0:
8 ¦ n -= 1
9
10 t1 = threading.Thread(target=count, args=(NUM,))
11 t2 = threading.Thread(target=count, args=(NUM,))
12 start = time.time()
13 t1.start()
14 t2.start()
15 t1.join()
16 t2.join()
17 print "multithread:"
18 print time.time() - start
19
20 start = time.time()
21 count(NUM)
22 count(NUM)
23 print "single thread:"
24 print time.time() - start
25
26 p1 = multiprocessing.Process(target=count, args=(NUM,))
27 p2 = multiprocessing.Process(target=count, args=(NUM,))
28 start = time.time()
29 p1.start()
30 p2.start()
31 p1.join()
32 p2.join()
33 print "multi process:"
34 print time.time() - start
Here’s the output:
multithread:
1.70929884911
single thread:
1.03298616409
multi process:
0.507339954376
Why do I get those performance results?
We can think of category theory as a generalized set theory, where in set theory we have sets and $\in$, but in category theory we have objects and arrows, where arrows are just any kinds of mappings.
So we have a kind of composition structure, where ther order of composition doesn’t matter, but the configuration matters.
And rather than reasoning structurally like PL does, it reasons “behaviorally”.
The main question is, how do we define two programs are equal, and how do we prove it.
So for setup we have type $int$, and $k$ which is a $int$, and $e_1+e_2$.
Family of types is a generalization of the concept of a predicate/relation.
Formally, given a type $A:U$ in a universe of types $U$, one may havea family of types $B:A\rightarrow U$, which assigns to each term $a:A$ a type $B(a):U$. We say that the type $B(a)$ varies with $a$.
e.g.
the following proposition
is a predicate / propositional function / a family of types (indexed by ) / fibration. We can rewrite it as
The idea is that we are exhibiting a family of types/proofs in that if you give me any particular choice of number, it’s going to give me back a proposition, which may or maynot be inhabitied, but they are all types.
For example, will be uninhabited, and will be inhabitited.