Custom typeclass instances problem

Stream: new members

[Rado Kirov]

In the following example, I am trying to build a custom type-class instance and pass it in manually with @, but it seems that the presence of the (T: Test \a) instance that I need to construct the new instance messes Lean up.

Is there a way to fix this without turning Opp into a typeclass and creating type aliases for \a?

import Mathlib

class Test (α : Type*) where
  foo: ℤ

def Opp (α: Type*) (T : Test α) : Test α where
  foo := -T.foo

structure D (α : Type*) [Test α] where
  bar : ℤ

def test (α: Type*) (T: Test α) : @D α (Opp α T) where
  bar := 0

[Kenny Lau]

@Rado Kirov the where etc stuff is a sugar which calls D.mk and as you might expect, calling D.mk will trip Lean up, so you can just not use the where syntax and call the underlying D.mk directly:

import Mathlib

class Test (α : Type*) where
  foo: ℤ

def Opp (α: Type*) (T : Test α) : Test α where
  foo := -T.foo

structure D (α : Type*) [Test α] where
  bar : ℤ

def test (α: Type*) (T: Test α) : @D α (Opp α T) :=
  @D.mk α (Opp α T) 67

[Kenny Lau]

in general Lean has way more sugar than you would expect, everything you see is basically sugar

[Rado Kirov]

There used to be a joke in PL that too much syntactic sugar leads to cancer of the semi-colon :)

[Rado Kirov]

Anyways, this is a great answer! It is actually a very simple answer, where bar := 67 is implicitly D.mk 67, so obviously I didn't pass the right instance with @D.mk.

The error is a very obvious type error between the declared and inferred type, I just couldn't see the explicit call to D.mk because it was behind the sugar. Thank you!

[Kenny Lau]

Kenny Lau said:

everything you see is basically sugar

def is a sugar, : is a sugar, := is a sugar, () is a sugar, ...

[Kenny Lau]

oh the more obvious one, Type* is a mathlib sugar

[Rado Kirov]

from the constructs I see, what is not sugar?

[Kenny Lau]

oh yeah, even the variable names are sugar, they're really db (de Bruijn) indices

[Kenny Lau]

I guess the constant names are real (Test, Opp, D, test) and that's pretty much it

[Rado Kirov]

well, now you are being facetious :) It's all electrons moving around and it's all sugar on top.

In PL, syntactic sugar, generally means something more specific, that the syntax is manupuled to some new form and that operates before some other part of the compiler/type-checker that works with fewer concepts.

[Rado Kirov]

The problem is I am reading an error from the type checker that sees desugared terms, and I am looked at sugared and we can't share our understanding.

[Kenny Lau]

anyway, we know where the error is now

[Kenny Lau]

Rado Kirov said:

In PL, syntactic sugar, generally means something more specific, that the syntax is manupuled to some new form and that operates before some other part of the compiler/type-checker that works with fewer concepts.

the thing is, lean is its own meta language, which makes your classification more complicated maybe

[Rado Kirov]

Defintely, it's the fanciest most powerful language I have ever seen, but even simpler languages like TypeScript can be a mess to work with once you go in the deep end.

[Rado Kirov]

And this is all just doing math with Lean, which means no worry about execution model

[Rado Kirov]

Feeling like I want to read (or write since I can't find any) a blog post around the four ways of doing implicit stuff with Lean:

• inference with _
• inference with {}
• type-class inference with []
• variable / auto-implicit
  I think it is where the intermediate Lean user struggles most. I feel like I have seen a post like this in https://xenaproject.wordpress.com/ but I can't find it?

[Rado Kirov]

I think @Dan Abramov has a bit - https://overreacted.io/a-lean-syntax-primer/#implicit-arguments but the interesting question to me is when one is writing some new math, how to best use these utilities.

[Rado Kirov]

Something like this

import Mathlib

/-!
Example of progressively using fancier Lean strucutres to improve
proof reuse and remove visual clutter

n and hn are very contrived here for simplicity, but imagine
a much more complicated bundle of data and properties that
repeats
-/

-- beginner Lean - only explicit terms
theorem t1 (n: ℕ) (hn: n > 0) : n + 1 = 1 + n := by sorry
theorem t2 (n: ℕ) (hn: n > 0) : n + 2 = n * n := by sorry
theorem t3 (n: ℕ) (hn: n > 0) : n * 2 = 2 * n := by
  have h1 := t1 n hn
  have h2 := t2 n hn
  sorry

-- step one
-- notice n is inferable from hn -> use implicit args
theorem t1s1 {n: ℕ} (hn: n > 0) : n + 1 = 1 + n := by sorry
theorem t2s1 {n: ℕ} (hn: n > 0) : n + 2 = n * n := by sorry
theorem t3s1 {n: ℕ} (hn: n > 0) : n * 2 = 2 * n := by
  have h1 := t1s1 hn
  have h2 := t2s1 hn
  sorry

-- step two - pack n and hn using structures
-- this is most natural to a software programmer, but doesn't look good
-- because of all the hp.n now
structure PosN where
  n: ℕ
  hn: n > 0

theorem t1s2 (hp: PosN) : hp.n + 1 = 1 + hp.n := by sorry
theorem t2s2 (hp: PosN) : hp.n + 2 = hp.n * hp.n := by sorry
theorem t3s2 (hp: PosN) : hp.n * 2 = 2 * hp.n := by
  have h1 := t1s2 hp
  have h2 := t2s2 hp
  sorry

-- step two' - pack n and hn using subtypes, not much better
def PosN2 := {x : ℕ // x > 0}
theorem t1s2' (hp: PosN2) : hp.val + 1 = 1 + hp.val := by sorry
theorem t2s2' (hp: PosN2) : hp.val + 2 = hp.val * hp.val := by sorry
theorem t3s2' (hp: PosN2) : hp.val * 2 = 2 * hp.val := by
  have h1 := t1s2' hp
  have h2 := t2s2' hp
  sorry

-- step three type classes
class PosNT (n: ℕ) where
  hn : n > 0

-- look ma, no args
theorem t1s3 {n: ℕ} [PosNT n] : n + 1 = 1 + n := by sorry
theorem t2s3 {n: ℕ} [PosNT n] : n + 2 = n * n := by sorry
theorem t3s3 {n: ℕ} [PosNT n] : n * 2 = 2 * n := by
  have h1 := t1s2'
  have h2 := t2s2'
  sorry

ok at this point might as well write the blogpost.