Re: Axiom musings ... runtime computation of first-class dependent types

Tim, Thanks for your reply, lots to think about in this subject isn't there. Like you I'm attempting the daunting (but interesting) path of trying to understand this subject better. Dependent types allow functions to exist in the type definition. The functions can be executed "at run time".

Re: Axiom musings ... runtime computation of first-class dependent types

Martin, >In this series of videos Robert Harper gives an provocative take on >these subjects: >https://www.youtube.com/watch?v=LE0SSLizYUI I watched Harper's videos years ago. I will revisit them. If you haven't seen them I highly recommend them.

Re: Axiom musings ... runtime computation of first-class dependent types

Tim In this series of videos Robert Harper gives an provocative take on these subjects: https://www.youtube.com/watch?v=LE0SSLizYUI At about 37 min into this video he says: "what is true has unbounded quantifier complexity whereas any formalism is always relentlessly recursively

Axiom musings ... runtime computation of first-class dependent types

Well, SANE is certainly turning into a journey. When we look at the idea of first-class dependent types as implemented in languages like Agda and Idris we find what I call "peano types". For example, Fin is a type of "finite numbers", usually defined as data Fin : Nat -> Type where FZ : Fin (S