Skolem is used to identify type abstractions. FIXME: not sure.

From the data Type, we can see something about PS's type system:

About "row polymorphism":

> let showPerson { first: x, last: y } = y ++ ", " ++ x
> :type showPerson
forall r. { first :: String, last :: String | r } -> String

This means that as long as a record has same fields first and last, the function application is well-typed. The r row is a polymorphic variable.

But type of record is RCons String Type Type? It seems to be a recursive construct:

rowToList :: Type -> ([(String, Type)], Type)
rowToList (RCons name ty row) = let (tys, rest) = rowToList row
                                in ((name, ty):tys, rest)
rowToList r = ([], r)

So, a somewhat unclear r will be returned. FIXME: How is such r treated in inference process.

And a lot of every everyWhereOnTypesXXX ... How can I comment ....


Easy to see, the type system of PureScript is no less than powerful. I think currently the most complex part in the compiler should be type checker ... But here we also have problems:

  • Is the checking algorithm efficient?
  • Is the type checking pipeline easy to maintain?

The first one effects the compilation speed greatly, while the second one is important, if you want to extend the type system in some way.