Stream: General

Topic: translations with ambiguous types

Kevin Kappelmann (Jan 19 2022 at 16:01):

I am trying to define translations for function spaces. There are different function spaces for individuals i and types t.
Is there some way to make all of the following type? Sadly(?), there is no filtering/backtracking for translations according to the reference manual

theory Scratch
  imports HOL.HOL
begin

typedecl i
typedecl t

consts
  set_dep_fun :: "i ⇒ (i ⇒ i) ⇒ i"
  type_dep_fun :: "t ⇒ (i ⇒ t) ⇒ t"
  elem :: "i ⇒ i ⇒ bool" (infix "∈" 50)
  has_type :: "i ⇒ t ⇒ bool" (infix ":" 50)

abbreviation "set_fun A B ≡ set_dep_fun A (λ_. B)"
abbreviation "type_fun A B ≡ type_dep_fun A (λ_. B)"

syntax
  "_telescope" :: "logic ⇒ logic ⇒ logic"  (infixr "→" 55)
translations
  "(x ∈ A) args → B" ⇀ "(x ∈ A) → args → B"
  "(x ∈ A) → B" ⇌ "CONST set_dep_fun A (λx. B)"

  "(x : A) args → B" ⇀ "(x : A) → args → B"
  "(x : A) → B" ⇌ "CONST type_dep_fun A (λx. B)"
  (* Optimally, instead of the next two translations, I would love to say:
     if `A → B` is of type `t` then use `type_fun` otherwise use `set_fun`. *)
  "(A :: t) → B" ⇌ "CONST type_fun A B"
  "A → B" ⇌ "CONST set_fun A B"

declare [[show_types]]
term "(x ∈ A) → B x"
term "(x : A) → B x"
term "A → (x ∈ B) → (C x)"
term "(A :: i) → (x ∈ B) → C x" (*same as line above*)
term "(A :: t) → (x : B) → (C x)"
term "(x ∈ A) → B → C x"
term "(x : A) → (B :: t) → C x"
term "(x : A) → B → C x" (*fails*)
term "A → B"
term "(A :: i) → B" (*same as line above*)
term "(A :: t) → B"
term "(A → B) :: t" (*fails*)
term "(A → B) = ((x ∈ A) → B)"
term "((A :: t) → B) = ((x : A) → B)"
term "(A → B) = ((x ∈ A) → B)"
term "(A → B) = ((x : A) → B)" (*fails*)

end

Lukas Stevens (Jan 19 2022 at 16:09):

I am not sure how this stuff works but could you use a parse translation? In a parse translation you can use arbitrary ML code to produce the result.

Manuel Eberl (Jan 19 2022 at 16:22):

I may be mistaken about this, but don't translations (including parse translations) work entirely on the syntactic stage, i.e. before the terms even have any type information at all?

Manuel Eberl (Jan 19 2022 at 16:24):

In that case, I think the only way to achieve what you want to do would be to add a checking stage that changes the placeholder constant of the input syntax into what you actually want it to be as soon as the type is known.

Manuel Eberl (Jan 19 2022 at 16:24):

This is pretty much what adhoc_overloading does.

Manuel Eberl (Jan 19 2022 at 16:25):

Of course, there is the fundamental problem of "what happens if the type is neither i nor t", or if the type is completely polymorphic. (adhoc_overloading then fails with an error message)

Manuel Eberl (Jan 19 2022 at 16:26):

Such additional checking phases are also notoriously problematic when you have several of them, since they can then interact with each other poorly (e.g. adhoc_overloading plus coercions)

Manuel Eberl (Jan 19 2022 at 16:26):

Then again I may also have completely misunderstood what you are trying to do; in that case just ignore my ramblings.

Kevin Kappelmann (Jan 19 2022 at 16:36):

As far as I can see (having skimmed the documentation), you are right Manuel and an additional phase during type checking would be necessary.

Last updated: Apr 20 2024 at 01:05 UTC