Stream: Beginner Questions

Topic: generic-length uncurrying function

view this post on Zulip Alicia (Apr 29 2025 at 11:04):

Hello, be warned: I am not that deep into simple type theory so my question might be incredibly stupid from a theoretical standpoint alone... Is there a way to define a function that does generic length uncurrying? That is, I'm looking for a function that takes as argument any curried function 

f :: t_1 => t_2 => ... => t_n

of arbitrary length n and returns a function 

g :: (t_1 x t_2 x ... x t_{n-1}) => t_n

Thank you very much in advance!

view this post on Zulip Jan van Brügge (Apr 29 2025 at 13:16):

No, that is not possible

view this post on Zulip Dmitriy Traytel (Apr 30 2025 at 13:06):

With overloading one can get pretty far actually.

consts uncurry :: "('A ⇒ 'B) ⇒ 'C ⇒ 'D"

overloading uncurry_fun ≡ "uncurry :: ('a ⇒ 'b ⇒ 'c) ⇒ 'a × 'B ⇒ 'C"
begin
definition uncurry_fun :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a × 'B ⇒ 'C" where
  "uncurry_fun f = (λ(a, b). uncurry (f a) b)"
end
overloading uncurry_unit ≡ "uncurry :: ('a ⇒ 'b) ⇒ (unit ⇒ 'a) ⇒ 'b"
begin
definition uncurry_unit :: "('a ⇒ 'b) ⇒ (unit ⇒ 'a) ⇒ 'b" where
  "uncurry_unit f g = f (g ())"
end

lemma "uncurry f (a, λ(). b) = f a b"
  unfolding uncurry_fun_def uncurry_unit_def prod.case unit.case ..
lemma "uncurry f (a, b, λ(). c) = f a b c"
  unfolding uncurry_fun_def uncurry_unit_def prod.case unit.case ..
lemma "uncurry f (a, b, c, λ(). d) = f a b c d"
  unfolding uncurry_fun_def uncurry_unit_def prod.case unit.case ..
lemma "uncurry f (a, b, c, d, λ(). e) = f a b c d e"
  unfolding uncurry_fun_def uncurry_unit_def prod.case unit.case ..

view this post on Zulip Dmitriy Traytel (Apr 30 2025 at 13:09):

Above I use the unit type to stop the overloaded recursion.

view this post on Zulip Dmitriy Traytel (Apr 30 2025 at 13:10):

Probably it would be safer to introduce a new dummy type for this purpose---the unit type might have other legitimate uses.

view this post on Zulip Dmitriy Traytel (Apr 30 2025 at 13:15):

I.e. something like this:

consts uncurry :: "('A ⇒ 'B) ⇒ 'C ⇒ 'D"
datatype 'a stop_curry = Stop_Curry (get_curry: 'a) ("$_")

overloading uncurry_fun ≡ "uncurry :: ('a ⇒ 'b ⇒ 'c) ⇒ 'a × 'B ⇒ 'C"
begin
definition uncurry_fun :: "('a ⇒ 'b ⇒ 'c) ⇒ 'a × 'B ⇒ 'C" where
  "uncurry_fun f = (λ(a, b). uncurry (f a) b)"
end
overloading uncurry_stop_curry ≡ "uncurry :: ('a ⇒ 'b) ⇒ 'a stop_curry ⇒ 'b"
begin
definition uncurry_stop_curry :: "('a ⇒ 'b) ⇒ 'a stop_curry ⇒ 'b" where
  "uncurry_stop_curry f g = f (get_curry g)"
end

lemma "uncurry f (a, $b) = f a b"
  unfolding uncurry_fun_def uncurry_stop_curry_def prod.case stop_curry.sel ..
lemma "uncurry f (a, b, $c) = f a b c"
  unfolding uncurry_fun_def uncurry_stop_curry_def prod.case stop_curry.sel ..
lemma "uncurry f (a, b, c, $d) = f a b c d"
  unfolding uncurry_fun_def uncurry_stop_curry_def prod.case stop_curry.sel ..
lemma "uncurry f (a, b, c, d, $e) = f a b c d e"
  unfolding uncurry_fun_def uncurry_stop_curry_def prod.case stop_curry.sel ..

view this post on Zulip Jan van Brügge (Apr 30 2025 at 13:59):

ok, but that is not just one function, yes with workarounds one can achieve something similar. Usually in this cases however it is better to ask "what are you trying to achieve" and find a better wax to express it

view this post on Zulip terru (Apr 30 2025 at 14:02):

If you're willing to go down this route, I don't quite see why you need the extra marker to stop the recursion? You can replace the uncurry_unit of Dmitriy's first listing with:

overloading uncurry_unit ≡ "uncurry :: ('a ⇒ 'b) ⇒ 'a ⇒ 'b"
begin
definition uncurry_unit :: "('a ⇒ 'b) ⇒ 'a ⇒ 'b" where
  "uncurry_unit f g = f (g)"
end

and still get

lemma "uncurry f (a, b, c, d) = f a b c d"
  unfolding uncurry_fun_def uncurry_unit_def by simp

as expected. However, note that type inference in the presence of this uncurry (and overloaded constants more generally) becomes supremely annoying:

term "uncurry f (a,b,c,d)" (* infers 'g for this expression, instead of `'a => 'b => 'c => 'd => 'e` *)

lemma "uncurry (λa b c d. d) (a,b,c,d) = d" oops (* unprovable since it infers different types for a,b,c,d each time *)

lemma "uncurry (λ(a::'a) (b::'b) (c::'c) (d::'d). d) (a::'a,b::'b,c::'c,d::'d) = (d::'d)"
  unfolding uncurry_fun_def uncurry_unit_def by simp (* goes through *)

So this is a fun corner of Isabelle, but as Jan says, probably not what you actually want to do ;)

view this post on Zulip Dmitriy Traytel (Apr 30 2025 at 17:02):

Ah, I thought I need some special type as a marker to make the cases non-overlapping--- but indeed they already are non-overlapping. Nice @terru.

I agree that the entire overloading approach may not be what one should use, especially not as a beginner. But I felt triggered by Jan's categorical statement. :smile:

Last updated: May 09 2025 at 08:28 UTC