Ant S. (Sep 22 2026 at 16:34): Ant S. (Sep 22 2026 at 16:34):It seems to me that proving an arbitrary property over an n-ary HOL function of type (a1 => (a2 => ... (an => b))) is not possible, since STT doesn't permit quantifying over types themselves. Is there some sort of smart workaround that I can use to prove properties over n-ary (curried or uncurried) functions
Ant S. (Sep 22 2026 at 16:34):(note: n is variable)
Mathias Fleury (Sep 22 2026 at 17:32):fold + lists is a workaround
Ant S. (Sep 22 2026 at 17:46):wouldn't that work if all of the a_i are the same type
Ant S. (Sep 22 2026 at 17:46):which they aren't?
Ant S. (Sep 22 2026 at 17:46):since lists are homogenous
Mathias Fleury (Sep 22 2026 at 17:49):Correct, but usually n-ary operators have a fixed type as argument...
Mathias Fleury (Sep 22 2026 at 17:49):(at least in my experience)
Ant S. (Sep 22 2026 at 17:56):I'm guessing I'm making an X-Y problem here, sorry about that.
I'm trying to get the hang of HOLCF. What I'd like to prove is that if (σ1, ... σn) are all flat types, then (σ1 -> (σ2 -> ... -> (σn -> τ))) that is strict in its first n arguments is monotonic (Logic and Computation, exercise 3.4)
Ant S. (Sep 23 2026 at 14:39):(typo: exercise 3.3)
Last updated: Sep 28 2026 at 16:33 UTC