I've implemented a completely functional DSL, and now I'd like to reason about it. It would be helpful to be able to compare it to existing languages.
The type system is parametric polymorphic with higher order functions but no dependent types. The only recursion allowed is structural recursion in the form of a fold over an inductively defined type (including natural numbers).
The way I see it, the language shares its turing-incompleteness and form of recursion with Coq, but shares parametric polymorphism with Haskell. Is there a more exact comparison to be made? In particular, I was wondering if System F can be pared down to only support structural recursion, and what that would look like.
Thanks!