Language/type system closest to Haskell without general recursion

Question

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!

Answer 1

The language closest to Haskell without general recursion is Haskell without general recursion, with suitable fold operations taken as primitive.

Haskell's datatypes have non-wellfounded values thanks to Haskell's lazy evaluation strategy. Once we remove general recursion from Haskell, the difference between lazy and eager evaluation does not matter anymore, and the datatypes become inductive in the sense that only well-founded values may be expressed (because every program is terminating, and folding over an non-wellfounded value woudl give a non-terminating program). So, you can just keep Haskell without general recursion, it's got parametric polymorphism, and the inductive types will work as expected.