PureScript type system name

4
votes

What is the proper academic name for the type system used in PureScript? I am looking for papers about that and proofs that it is sound.

In particular, as the type system allows to solve the exception as hidden communication channel problem when one wants to throw an instance of private exception type and pass it through effectful computations to the catch handler without the need to expose the type to the computation and possibility to catch it there, it would be nice to confirm that this is sound.

1
purescript

1 Answers

17
votes

The PureScript type checker isn't based on any one type system in particular. I took inspiration from several papers as I implemented it, including:

  • "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism" by Joshua Dunfield and Neelakantan R. Krishnaswami
  • "HMF: Simple Type Inference for First-Class Polymorphism" by Daan Leijen
  • "Koka: Programming with Row-polymorphic Effect Types" by Daan Leijen

There are no soundness proofs. At some point, I would be interested in going back and reimplementing the type checker based on some system with soundness guarantees, but the initial goal was to produce a practical type system with the features that I wanted: row polymorphism, type classes and rank N types.