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

Like
Like Love Haha Wow Sad Angry
2511

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
2511

Demystifying the Type Declarations in C

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

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

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

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

Like
Like Love Haha Wow Sad Angry
1

An incident caused by an incorrect TypeScrpit type definition of Mongoose

Like
Like Love Haha Wow Sad Angry
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";
      }
    });
})

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

Like
Like Love Haha Wow Sad Angry
2

A random ride

Like
Like Love Haha Wow Sad Angry
1

After taking part in the discussion in preparation of the presentation for the course “British History and Classical Texts”, I was on the way to Walmart for cheeses, when I suddenly discovered I took no money with me. While with the new decision to simply ride downtown, I actually ended up arriving at the MIXC (万象城) distant from the center. Since I had no money, I could do nothing but take photos…

Ralf Lauren的童裝櫥窗,擺設得有點意思。
Showcase of Ralf Lauren Kids

I actually intended to park at the Xinhua bookstore on Qingchun road and have a look. However, I forgot that when I was regretting on not taking any money and not being able to buy cheeses. There is also a bookstore in MIXC though. It’s called Page One, and sells mostly petite bourgeoisie books, e.g. on interior design, cooking, literature, history and philosophy, many of which are in English.

Continue reading “A random ride”

Like
Like Love Haha Wow Sad Angry
1

What are the stories/allusions behind these untranslatable words?

Like
Like Love Haha Wow Sad Angry

It seems that the picture is from tumblr. It was written in English, and became more verbose when translated to Chinese. But are all the words necessary? The original writer could be attracting attentions by such verbosity.

And many of the words (including but not restricted to the ones I know) aren’t curious at all.

waldeinsamkeit = wald + einsamkeit = forest + loneliness = 林中孤獨(孤感?)
почемучка = почему + чка = 爲什麼 + 指小的後綴,實則專指小孩,《简明俄汉词典》的“小問號”之譯乃至勝過原詞。
木漏れ日 = 木(樹) +漏れ(漏れる)+ 日(太陽),譯作漢語也許去掉假名即可。
dépaysement = dépayse(r) + ment,化dépayser(離鄉,或者「遷」我看就行)爲名詞。有的詞典作好感,有的詞典作不適,還有一「流放」的廢意。「離鄉」之類也是古意。

Continue reading “What are the stories/allusions behind these untranslatable words?”

Like
Like Love Haha Wow Sad Angry

Why do ancient Chinese portraits look so unreal?

Like
Like Love Haha Wow Sad Angry
11
我觉得某些回答的某些部分是很有误导性的。比如 @张佳玮 拿一副古埃及的壁画和唐代画比,那可是公元前 1000 年以前的作品,而且这种画风至少公元前 3000 年以前就定型了,再说并不一定埃及就能代表西方,埃及没有写实绘画(其实罗马化还是有的)不代表希腊罗马没有。比如 @沈临枫 拿兵马俑当作写实的证据,未免有些太没说服力了。画说在前头,底下举一些例子(来自维基百科)。
 
Facsimile of the Narmer Palette, c. 3100 BC,跟那种画一个风格。
用户上传的图片
 
 
跟埃及人比也可以。。可以比雕塑,比如拿木乃伊的面具嘛,或者古埃及也有雕塑。
King Menkaura (Mycerinus) and queen, Egyptian, Old Kingdom, Dynasty 4, reign of Menkaura, 2490–2472 B.C.
 

Continue reading “Why do ancient Chinese portraits look so unreal?”

Like
Like Love Haha Wow Sad Angry
11

Reading Russian Lines of Cloud Atlas (4)

Like
Like Love Haha Wow Sad Angry

ОБЛАЧНЫЙ АТЛАС

Острова Тихого Океана, 1849 год.

Дело сделано, мистер Юинг, теперь сей контракт свят для исполнения… почти как Десять Заповедей.

сделано: done
сей: this
свят: holy
исполнения: execution, fulfillment
почти: almost
Заповедей: commandment

Благодарю, Преподобный Хоррекс, мой тесть с нетерпением ждёт завершения этой сделки.
Преподобный: Reverend
тесть: father-in-law
нетерпением: impatience, hurry
ждёт: wait for, expect
завершения: completion
сделки: transaction Continue reading “Reading Russian Lines of Cloud Atlas (4)”

Like
Like Love Haha Wow Sad Angry

Reading Russian Lines of Cloud Atlas (3)

Like
Like Love Haha Wow Sad Angry

– Здравствуйте.
– Ваш пропуск.
Смотрю вы начеку?

пропуск: pass, admission
начеку: on the alert


Я был издателем Дермонта Хоггинса, а не психоаналитиком или астрологом, и это чёртова, чёртова правда, я и понятия не имел, что он сделает в тот вечер.

издателем: publisher
психоаналитиком: psychoanalyst
астрологом: astrologer
понятия: idea
имел: have
тот: that
вечер: evening

Continue reading “Reading Russian Lines of Cloud Atlas (3)”

Like
Like Love Haha Wow Sad Angry

Quotes From Cloud Atlas (I)

Like
Like Love Haha Wow Sad Angry

Теперь я понимаю, что границы между шумом и звуком условный. Любые границы условный, и созданный, чтобы их переступать. Всё условности преодолимый, стоит лишь поставить для себя эту цель.

граница: limit, confine
между: between
шум: noise Continue reading “Quotes From Cloud Atlas (I)”

Like
Like Love Haha Wow Sad Angry

Polynomials and Power Series (I)

Like
Like Love Haha Wow Sad Angry

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

Reading Russian Lines of ‘Cloud Atlas’ (2)

Like
Like Love Haha Wow Sad Angry

Вот тогда-то я и свёл знакомство с доктором Генри Гуссом, с человеком, который, как я надеялся, сможет излечить мой недуг.
Вы что-то ищите?


тогда-то: then, at that time
свёл (свести): took; свёл знакомство с: made the acquaintance of
который: who
надеялся: hope
сможет: be able to
излечить: cure
недуг: ailment, illness
что-то: something
ищите: look for, search after

Continue reading “Reading Russian Lines of ‘Cloud Atlas’ (2)”

Like
Like Love Haha Wow Sad Angry

Discussion on Exercises of Commutative Algebra (I)

Like
Like Love Haha Wow Sad Angry

  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

A Simple Combinatorial Problem and Related Thoughts

Like
Like Love Haha Wow Sad Angry

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

Generating Functions and Formal Power Series

Like
Like Love Haha Wow Sad Angry

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

Reading Russian Lines of ‘Cloud Atlas’ (1)

Like
Like Love Haha Wow Sad Angry

Тоскливая ночь.
Обыватели печальный, ветер пробирает до костей.
В нём я слышу…голоса.
Это вой, вой предков, они рассказывают свои истории.
Их голоса сплетаются в хор.
Но один голос особенный…
Этот голос, шепчет, преследует тебя из мрака.
Клыкастый дьявол, сам Старина Джорджи.
Приготовитесь слушать, и я расскажу тебе о том, как мы встретились в первый раз, лицом к лицу.




Words:

Тоскливая: depressed, sad
ночь: night

Continue reading “Reading Russian Lines of ‘Cloud Atlas’ (1)”

Like
Like Love Haha Wow Sad Angry

A Quote From ‘Cloud Atlas’

Like
Like Love Haha Wow Sad Angry
На улице тяжёлый снег падал на шиферные крыши и гранитные стены. Подобно Солженицыну, томившемуся в Вермонте,
я буду трудиться
в изгнании.
Но в отличие от Солженицына, я буду не один.



Explanation:

green: radical
red: prefix
blue: suffix
dark red: preposition
orange: auxiliary ingredients
purple: declension
grey
background
: accent

 

 

underline: proper noun
Friday, July 12, 2013
Like
Like Love Haha Wow Sad Angry

Faith

Like
Like Love Haha Wow Sad Angry

When I was a child, I was attracted by the world beyond our planet. I did not have the opportunity to see a really starry night, for the I did not often live in the country side. But I could still imagine. I bought I lot of books which introduced efforts humans had made on exploring the outer world. I also watch cartoons related to this topic. My yearning for the vast world first led me to science.

Years have passed. Now I’ve been concentrating on mathematics. But the deep spaces still play an important role in my life. I am not fond of money, honor, reputation or something else, for I believe that there is something far greater. Money, honor or reputation only works in human society and the duplicity, deception and disguise intended for these things are simply nothing but abjection in front of the universe. Continue reading “Faith”

Like
Like Love Haha Wow Sad Angry

An Animation and the Middle Age

Like
Like Love Haha Wow Sad Angry
1

This weekend I came across the anime Spice and Wolf. The character Horo is so cute, but this is not what I want to mention most.

It was in the Middle Age, Lawrence, the main character is a travelling merchant. Therefore trading activities and religious organizations(sorry I can’t find an equivalent word) are often mentioned in the story. That inspired me to the imagination of the Middle Age.

It was a dark age that religious power controlled the society, and however, an age of merchants. There were villages, towns, cities, ports and kingdoms. There were missionaries, knights, mercenaries and kings. It was hard to transmit information. It was hard to transport substances. It was a solid age. And it was merchants, who traveled everywhere for more benefits, that liquefied the age. Continue reading “An Animation and the Middle Age”

Like
Like Love Haha Wow Sad Angry
1

Diary (Sep 4, 2010)

Like
Like Love Haha Wow Sad Angry

The book From Calculus to Cohomology by Madsen looks a nice book. Well, it’s the first time I saw an introduction to topology from CALCULUS so I believe it amazing. Maybe I am too ignorant in mathematics.

I’m studying Commutative Algebra and Topology recently. As far as I’m concerned, categories are fundamental in mathematics so I’m particularly fond of algebra in favor of the concept of category. I saw some one says geometry and topology structures are much more interesting than algebra structures. I don’t understand it very much. Maybe in my mind all structures are algebraic. Well, maybe when we adopt measures and Cauchy sequences we are entering the field of Analysis, Geometry and Topology? Actually in my heart it is still algebraic. I think continuity doesn’t mean non-algebra. Continue reading “Diary (Sep 4, 2010)”

Like
Like Love Haha Wow Sad Angry