What is GADT (Generalized Algebraic Data Types) in Haskell?

Like
Like Love Haha Wow Sad Angry
3912

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?”

Like
Like Love Haha Wow Sad Angry
3912

Demystifying the Type Declarations in C

Like
Like Love Haha Wow Sad Angry
921
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[5]; // With 5 elements.

Are you able to declare a pointer?

int *a;

Nested Twice

Are you able to declare a nested pointer?

Continue reading “Demystifying the Type Declarations in C”

Like
Like Love Haha Wow Sad Angry
921

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

Like
Like Love Haha Wow Sad Angry
4

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.

Continue reading “Implement Compile Time Peano Numbers – A Primer in C++ Template Metaprogramming”

Like
Like Love Haha Wow Sad Angry
4

An incident caused by an incorrect TypeScrpit type definition of Mongoose

Like
Like Love Haha Wow Sad Angry
4

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";
      }
    });
})

Continue reading “An incident caused by an incorrect TypeScrpit type definition of Mongoose”

Like
Like Love Haha Wow Sad Angry
4

Polynomials and Power Series (I)

Like
Like Love Haha Wow Sad Angry
2

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.
Like
Like Love Haha Wow Sad Angry
2

Discussion on Exercises of Commutative Algebra (I)

Like
Like Love Haha Wow Sad Angry
2

  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)”
Like
Like Love Haha Wow Sad Angry
2

A Simple Combinatorial Problem and Related Thoughts

Like
Like Love Haha Wow Sad Angry
2

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”

Like
Like Love Haha Wow Sad Angry
2

Generating Functions and Formal Power Series

Like
Like Love Haha Wow Sad Angry
2

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 ith and i+1th 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

Like
Like Love Haha Wow Sad Angry
2

On Zhang Yuzhe and Beyond

Like
Like Love Haha Wow Sad Angry
4

When I was in grade 1, I was reading a book, whose name I have forgotten, on the universe, stars, astronomy and so. There was a counterpart on earth. I just liked such books so much at that time, that I bought them sets by sets. One day I was reading a passage on the lunar and solar eclipses, which was saying that even though the solar eclipses happen more often that the lunar ones, most people would only have the chance to see lunar eclipses but not solar eclipses throughout their life. Why? Because each solar eclipse is only visible to a small region on the earth since the moon is small compared to the earth, while lunar eclipses are visible to half the earth (the half on the dark side). Moreover, solar eclipses are very short and susceptible to weather changes. Here comes an example on the book, that in some year (around 1970?)  there was a solar eclipse in China. Mr. Zhang Yuzhe who was already over 70 then hurried there for it. Unfortunately the eclipse was shadowed by the raining cloud. There was a portrait for Mr. Zhang Yuzhe on the page, who appears to be a thin, long-faced exotic-looking elderly. That aroused my interest for Mr. Zhang, but back then information communication was shabby. I was a little kid in a small town, without the Internet. How was I going to gather the related knowledge? But such curiosity wander in my mind, never disappearing. P.S. I was actually focus more on the “古稀” (over 70 years old) thing, firstly for I was almost illiterate and feeling fresh about this fancy word, secondly for it was emphasized somewhere else addressing life of human in the very book, that 70 years is equal to only about 20000 days, and that is “人生七十古來稀” (people hardly live up to 70 since the old days). I always felt pathetic about this, because books were mentioning that it would take over 200 years for Pluto to trip around the sun, and even for Halley’s comet it would take over 70 years.

There wasn’t Internet until many years later, when I entered the junior high. But I was then addicted to computer games (records of this period are in my Qzone. You can dive into it if your are interested.), and then to English, to mathematics, to politics, to digital devices. And I got oblivious to the astronomy things. Continue reading “On Zhang Yuzhe and Beyond”

Like
Like Love Haha Wow Sad Angry
4