Implicit type argument impossible to access?

Stream: lean4

[Niklas Halonen]

Hi all,

While defining Church booleans, I ran into an issue where it doesn't seem possible to specify a non-uniform implicit type argument.

Here's my code:

universe u
def Cbool := {T : Sort u} → T → T → T

#check Cbool            -- Cbool.{u} : Sort (imax (u + 1) u)
#check @Cbool Nat       -- error: function expected
#check Cbool (T := Nat) -- error: invalid argument name 'T'

-- How to unify T✝ with U?
def tt {U : Sort u} : Cbool := fun (x _y : U) => x

Is there a way to explicitly specify the type T for Cbool to be U?

[Edward van de Meent]

if you don't mind changing the definition a tad, this works:
def Cbool {T : Sort u} : Sort _ := T → T → T

[Edward van de Meent]

or, at least, i think it does?

[Edward van de Meent]

i might not completely understand your intention here

[Edward van de Meent]

reading your message again, i believe it might also be the case that you want (T → T) → T rather than T → T → T?

[Niklas Halonen]

Edward van de Meent said:

if you don't mind changing the definition a tad, this works:
def Cbool {T : Sort u} : Sort _ := T → T → T

Thanks for responding; unfortunately that makes handling the type parameter T very inconvenient and ugly:

def Cbool := {T : Sort u} → T → T → T
def ff : Cbool := fun _x y => y

-- This works and is pretty
def Cbool.and : Cbool → Cbool → Cbool := fun b1 b2 => b1 b2 ff
-- Method call (almost) works
#eval Cbool.to_bool <| ff.and ff -- false
#eval (ff.and ff).to_bool -- error: invalid field notation

-- However, moving the type parameter to be uniform

def Cbool' {T : Sort u} := T → T → T
def ff' : @Cbool' T := fun (_x y : T) => y

-- This doesn't work
def Cbool'.and : Cbool' → Cbool' → Cbool' := fun b1 b2 => b1 b2 ff'

-- This works but is too ugly
def Cbool'.and' : @Cbool' (@Cbool' T) → (@Cbool' T) → (@Cbool' T) := fun b1 b2 => b1 b2 ff'

-- Also methods don't work for some reason
#eval Cbool'.to_bool <| ff'.and' ff'

My current solution is to define the following Cbool hierarchy, which allows me to refer to the underlying type when necessary:

def CboolTTT {T : Sort u} {_t : T} {_t' : T} := T
def CboolTT  {T : Sort u} {t : T}            := (t' : T) → @CboolTTT T t t'
def CboolT   {T : Sort u}                    := (t : T)  → @CboolTT T t
def Cbool := {T : Sort u}                                → @CboolT T

-- Example for accessing the inner T type
def tt : @CboolT T := fun (x _y : T) => x

If you have better suggestions, please let me know!

[Kyle Miller]

There's a difference between

def Cbool := {T : Sort u} → T → T → T

and

def Cbool := fun {T : Sort u} => T → T → T

It seems like you're wanting to work with the first as if it were the second. Or maybe you want a feature that can specialize a pi type?

[Niklas Halonen]

Hmm, I think I get it. In the end I went with an explicit parameter def Cbool := (T : Type u) → T → T → T which made everything much easier :smiley: