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

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

Like
Like Love Haha Wow Sad Angry
3612

Demystifying the Type Declarations in C

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

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

Like
Like Love Haha Wow Sad Angry
2

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
2

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