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