half assed attempt at mimicking Arend

Stream: general

[Johan Commelin]

I just messed around a bit. Would be really awesome if something like this could work in Lean 4.
I think that bundling/unbundling is one of the major hurdles in making ITPs scale.
(I don't pretend that the following code is either deep or meaningful.)

universe variables u v

namespace test

instance fun_to_sig : has_coe_to_sort (Type u → Type u) :=
{ S := Type (u+1),
  coe := λ f, sigma f }

instance carrier (f : Type u → Type u) : has_coe_to_sort f :=
{ S := Type u,
  coe := λ X, X.1 }

def the_data {f : Type u → Type u} {X : f} : f X := X.2

variables (G : group)

instance group_inst : group G := the_data

lemma mul_inv {G : group} (x : G) : x * x⁻¹ = 1 :=
mul_inv_self x

variables (H : Type v) [comm_group H] (h : H)

def bundler {f : Type u → Type u} (X : Type u) [i : f X] : f := ⟨X, i⟩

notation `†` := bundler

#check (†H : group)

example : h * h⁻¹ = 1 := @mul_inv (†H) h

end test

[Scott Olson]

The most complete exploration of this bundling/unbundling design space that I've seen is The Next 700 Module Systems. It's implemented on top of Agda and is a little bit idiosyncratic, but it has a lot of ideas I dearly hope make their way into the mainstream soon.

[Bryan Gin-ge Chen]

Looks interesting! The preprint quotes the bit on structures from Tom Hales's "A review of the lean theorem prover" (point 10) and says "This is the problem we are solving."

[Scott Morrison]

It does look interesting! I'd really like to see how it works out with a non-trivial piece of mathematics (e.g. develop some of the theory of algebras over a ring).