Thoughts on API Design for Dependently-Typed Languages Posted on 2021-11-29idris type-systems dependent-types typing