# Language/type system closest to Haskell without general recursion

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!

• System F already only supports structural recursion! – cody Jan 25 '18 at 21:59
• @cody: maybe the poster thinks of system F + inductive types (instead of just negative encodings), and how to express recursive functions with structural recursion only there. (Which would suggest: a guard condition, or sized types, or compiling/elaborating pattern matching to eliminators). – gasche Jan 26 '18 at 9:19
• @gasche: yes, that is what I am thinking of! – lightning Jan 26 '18 at 17:04

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.