Generate curried function based on list?

Stream: Is there code for X?

[aron]

I'm trying to write a function that can convert a function that takes a list as input into a curried function. Something like this:

def makeCurriedType (t T : Type u) (n : Nat) : Type u :=
  if n = 0 then T else t → makeCurriedType t T (n - 1)


def convertToCurriedType {t T : Type u} (n : Nat) (f : List t → T) : makeCurriedType t T n :=
  let rec recursor (args : List t) (paramsRemaining : Nat) : makeCurriedType t T paramsRemaining :=
    match h : paramsRemaining with
    | 0 =>
      by
      have result := f args
      simp
      exact result

    | n + 1 =>
      by
      have nextFun := fun head => recursor (head :: args) n
      have : makeCurriedType t T (n + 1) = (t → makeCurriedType t T n) := by
        induction n with
        | zero =>
          simp
        | succ n hh =>
          simp at h
          rw [h] at hh
          sorry

      rw [this]
      exact nextFun

  recursor [] n

but I can't quite make it work. In particular I don't understand why hh is a function whose first parameter needs to be a proof that paramsRemaining = n.succ? Especially since that's impossible, since h : paramsRemaining = (n + 1).succ

[aron]

But to be honest I'd rather not use induction in the first place. Which I could do if there was a way for me to simp just one single recursive call of makeCurriedType. Then I could show that

makeCurriedType t T (n + 1) = (t → makeCurriedType t T n)

by definition.

Is there a way to do this? Unroll just one iteration of a recursive function?

[Eric Wieser]

makeCurriedType is docs#Function.OfArity

[aron]

ah nice. but the problem isn't with that, it's with convertToCurriedType

[Ilmārs Cīrulis]

I took liberty to redefine makeCurriedType. It seems that everything works that way.

import Mathlib

def makeCurriedType (t T : Type u) (n : Nat) : Type u :=
  match n with
  | 0 => T
  | m + 1 => t → makeCurriedType t T m

def convertToCurriedType {t T : Type u} (n : Nat) (f : List t → T) : makeCurriedType t T n :=
  let rec recursor (args : List t) (paramsRemaining : Nat) : makeCurriedType t T paramsRemaining :=
    match h : paramsRemaining with
    | 0 =>
      by
      have result := f args
      exact result
    | n + 1 =>
      by
      have nextFun := fun head => recursor (head :: args) n
      have : makeCurriedType t T (n + 1) = (t → makeCurriedType t T n) := by
        induction n with
        | zero =>
          simp
          rfl
        | succ n hh =>
          simp at h
          rw [h] at hh
          rfl
      rw [this]
      exact nextFun
  recursor [] n

[Eric Wieser]

I think you're overthinking this:

def convertToCurriedType {t T : Type u} (n : Nat) (f : List t → T) : Function.OfArity t T n :=
  match n with
  | 0 => f []
  | n + 1 => fun x => convertToCurriedType n (f <| x :: ·)

[Eric Wieser]

@Ilmārs Cīrulis is right that redefining makeCurriedType makes things easier, and indeed the new definition they use is now equal to the one OfArity produces

[Eric Wieser]

Though you can get there in even less code with

def convertToCurriedType {t T : Type u} (n : Nat) (f : List t → T) : Function.OfArity t T n :=
  Function.OfArity.curry fun args => f (.ofFn args)

[aron]

@Ilmārs Cīrulis oh nice. In fact if I use your definition of makeCurriedType things can be made even simpler:

def makeCurriedType (t T : Type u) (n : Nat) : Type u :=
  match n with
  | 0 => T
  | m + 1 => t → makeCurriedType t T m

def convertToCurriedType {t T : Type u} (n : Nat) (f : List t → T) : makeCurriedType t T n :=
  let rec recursor (args : List t) (paramsRemaining : Nat) : makeCurriedType t T paramsRemaining :=
    match paramsRemaining with
    | 0 => f args
    | n + 1 => fun head => recursor (head :: args) n

  recursor [] n

Why does that work when my original definition of makeCurriedType didn't? :thinking: is it because my definition didn't make it clear that the function terminates?

[Aaron Liu]

I'm thinking it might be because your original definition uses well-founded recursion

[Eric Wieser]

And probably also because n + 1 - 1 = n is not true by definition Nevermind, it is!