3612

We assume that you are familiar with what we are doing without GADT. Say, for the simplest case, we are defining a list：

List a = Nil | Cons a (List a)

What exactly are we doing?

• On the LHS, it defines a “type constructor” called List. It takes a type as parameter, and returns a new type. It’s essentially a function of types.
• On the RHS, it tells us that we have two ways to construct a value of type List a. One is called Nil and the other Cons a (List a).
• You can directly write Nil to get a value of type List a, with type a to be determined, more precisely inferred from the context.
• In the case of Cons a (List a), it’s actually a function named Cons, taking two parameters, one with type a, the other with type List a. Again, the type of a should be inferred from the context. But this time it’s often more direct, as a is the type of the first parameter.

Then we can represent these two constructors as normal functions: Continue reading “What is GADT (Generalized Algebraic Data Types) in Haskell?”

3612

## Demystifying the Type Declarations in C

621
The type declarations in C, restricted by C’s long history, appears rather complicated in many situations. Let’s give it a thorough analysis today.

# Pointers and Arrays

## Nested Once

Even the very beginners wouldn’t find the following problems hard:

Are you able to declare an array?

int a; // With 5 elements.

Are you able to declare a pointer?

int *a;

## Nested Twice

Are you able to declare a nested pointer?

621

## Implement Compile Time Peano Numbers – A Primer in C++ Template Metaprogramming

1

### Fundamentals

#### Function on Types

We all know that C++ templates can receive types as “parameters”. In the same spirit we could can “return values”s, so that we can form a function. The basic paradigm is the following:

template<class T>
struct Computed {
using type = T;
}

In this way we constructed a type level function named Computed, with one parameter  and result the parameter itself. We use the function as Computed<float>::type, the result being float itself.

1

## An incident caused by an incorrect TypeScrpit type definition of Mongoose

2

The TypeScript type definition of Mongoose are not fully correct!

I inspected (or debugged) a nodejs server project of Little Gengsha‘s, where he’s using koa as the server and mongodb as the data store. The project seems called “Writer’s Platform”, which seemed very primitive then. There were only two routes, a get, a post, the latter of which is used to submit an article to mongodb. During the test he discovered a problem — the body of the response should be changed in the callback of the save function, but the action response is “OK”, which is the default response of koa.

router.post('/path', (ctx, next) => {
const article = new Article( /* something */ );
article.save((err, article) => {
if (err){
ctx.body = err;
} else {
ctx.body = "success";
}
});
})
2

## Polynomials and Power Series (I)

Today we discuss something on polynomials.

### Over a Commutative Ring

Nilpotents and units are closely related. In a commutative unital ring $R$, if $x$ nilpotent, $a$ unit, then $a+x$ is again a unit. If $1+x y$ is a unit for every $y\in R$, then $x\in\mathfrak{R}$, the Jacobson radical, approximately nilpotent.

## Discussion on Exercises of Commutative Algebra (I)

1. Units
, nilpotents, and idempotents lift from $A/\mathfrak{N}$ to $A$.Proof: Units and nilpotents are obvious. In fact they lift to any of their representatives.
For idempotents, if $x^2=x\in A/\mathfrak{N}$, then $(1-x)x=0 \in A/\mathfrak{N}$, so $(1-x)^kx^k=0\in A$ for sufficiently large $k$. And $(1-x)^k+x^k=1-x+x=1\in A/\mathfrak{N}$, so lifts to a unit $(1-x)^k+x^k$. Moreover, its inverse $u=1\in A/\mathfrak{N}$. So $(ux)^k(u(1-x))^k=0,ux^k+u(1-x)^k=1\in A$ and $ux=x,u(1-x)=1-x\in A/\mathfrak{N}$.
This can be interpreted by sheaf theory, which is to be discussed in later posts. Continue reading “Discussion on Exercises of Commutative Algebra (I)”

## A Simple Combinatorial Problem and Related Thoughts

Problem: If the decimal expansion of $a$ contains all $10$ digits ($0,...,9$), then the number of length $n$ strings (shorted as $n$-strings) is greater than $n+8$.

If you’ve established the simple lemma, the solution is instant. Otherwise very impossible.

Lemma: The number $C_n$ of $n$-strings is strictly greater than $C_{n-1}$, that of $n-1$-strings.
Actually,  we always have $C_n \ge C_{n-1}$: Every $n-1$-string corresponds to an $n$-string by continuing 1 more digit. The map is clearly injective. If $C_n=C_{n-1}$, it is bijective, meaning we have a way to continue uniquely, which means rationality. Rigidly, at least one of the $n-1$-strings occurs infinitely, but all digits after some $n-1$-string is totally determined by it. So if an $n-1$-string appears twice, it must appear every such distances, and so do the digits between. Continue reading “A Simple Combinatorial Problem and Related Thoughts”

## Generating Functions and Formal Power Series

Today we discuss some generating functions.

Problem 1: Give a finite set of positive integers $T$. Let $\mathfrak{T}_n$ be the collection of sequences $(t_1,t_2,...,t_m)$, such that $\sum_{i=1}^m t_m=n$, and each $t_i\in T$. Let $a_n=|\mathfrak{T}_n|$ for $n\ge1$ and $a_0=1$, and $f(x)=\sum_{n=0}^{\infty}a_n x^n$. Find out what is $f(x)$ explicitly.

Solution: It is not hard to note the recursive relation $a_n=\sum_{t\in T} a_{n-t}$ for $n\ge1$, if we set $a_i=0$ for negative $i$. So that $f(x)=1+\sum_{t\in T} x^t f(x)$ and $f(x)=1/(1-\sum_{t\in T} x^t)$, which is a rational function.

Variantion 1: If $T$ is infinite, what would happen? Would $f(x)$ still be rational?

We first analyze simple cases. If $T=\mathbb{N}^+$, it is expected that $f(x)=1+\sum_{t=1}^{\infty} x^t f(x)=1+f(x) x/(1-x)$, so that $f(x)=(1-x)/(1-2x)=1+\sum_{n=1}^{\infty} 2^{n-1} x^n$. Indeed, in this case, counting the sequences amounts to divide a sequence of $n$ objects arbitrarily. You can choose to divide between the $i$th and $i+1$th for $1\ge i\ge n-1$, so in all $2^{n-1}$ choices, justifying the expansion.

I think it is equivalent to $f$ being rational.

Theorem: $\mathbb{Q}_p(t)\cap\mathbb{Q}[[t]]=\mathbb{Q}(t)$

It is very interesting that this theorem is used for the rationality of $\zeta$-functions for algebraic varieties, which is part of the Weil conjectures.

Wednesday, July 10, 2013

1