<p>The language closest to Haskell without general recursion is Haskell without general recursion, with suitable <code>fold</code> operations taken as primitive.</p>

<p>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 <code>fold</code>ing 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.</p>

CC BY-SA 3.0
2018-01-26T09:54:51.107Z
2018-01-26T09:54:51.107Z
Andrej Bauer
<p>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.</p>

<p>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).  </p>

<p>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.</p>

<p>Thanks!</p>

CC BY-SA 3.0
2018-01-25T21:59:22.823Z
System F *already* only supports structural recursion!
cody
CC BY-SA 3.0
2018-01-26T09:19:10.060Z
@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
CC BY-SA 3.0
2018-01-26T17:04:42.147Z
@gasche: yes, that is what I am thinking of!
lightning
<pl.programming-languages><type-theory><polymorphism>
Language/type system closest to Haskell without general recursion
lightning
# Language/type system closest to Haskell without general recursion

(Asked by: username_0 on 2018-01-25)

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!

**Tags:** pl.programming-languages, type-theory, polymorphism

> **Comments:**
> **username_1**: System F *already* only supports structural recursion!  
> **username_2**: @username_1: 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).  
> **username_0**: @username_2: yes, that is what I am thinking of!  

---

## 1 answers

### Answer by username_3 on 2018-01-26. Score: 3

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 `fold`ing 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.


---

