Pedal’s Type System

Pedal’s type system is a little unusual, trying to be internally consistent, simple, and easy to use. It is not a full type system, and it is not a full type checker. It is neither sound nor complete. It’s trying to be pedagogical, not practical.