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)
Alex Mobius (Oct 25 2026 at 18:38):In HOLCF, a good method to work over type-erased values is to work with deflations of udom. Each domain type has an associated DEFL(type) deflation. Sadly for some reason there isn't a standard symbol for "this udom value is of this type" judgment.
Functions do become awkward in this notation though.
Ant S. (Oct 25 2026 at 18:43):thanks! I've been meaning to grok udom one of these days (yes, I have been going through Brian Huffman's thesis, unless you have some other resources)
Last updated: Nov 08 2026 at 20:15 UTC