Zulip Chat Archive

Stream: new members

Topic: Can't display a number whose type is wrapped in a structure


Mike Shulman (Nov 18 2022 at 16:31):

Eric Wieser said:

This feels like an #xy problem

What do you think my X is?

Mike Shulman (Nov 18 2022 at 16:31):

Or maybe I should say, what makes you think what I'm asking about isn't my X? Isn't it reasonable to want to display things?

Mike Shulman (Nov 18 2022 at 16:32):

Alex J. Best said:

What do you mean by instance of wrap (instance is a keyword) are you varying wrapN or the class?

I mean different elements of wrap in which t is different.

Eric Wieser (Nov 18 2022 at 16:40):

I have no idea what your X is, but I'm very skeptical that structure wrap := (t : Type) is something you want to go anywhere near

Johan Commelin (Nov 18 2022 at 16:41):

Well, we have newtypes like that in mathlib in several places.

Eric Wieser (Nov 18 2022 at 16:41):

Do we? Can you give an example?

Eric Wieser (Nov 18 2022 at 16:41):

Category theory is maybe the only place I can think of

Johan Commelin (Nov 18 2022 at 16:41):

But usually they are very much on a one-off basis, and so reimplementing a couple of typeclasses is not a problem.

Johan Commelin (Nov 18 2022 at 16:43):

For example, we have something like

structure real :=
(cauchy : @cau_seq.completion.Cauchy  _ _ _ abs _)

Johan Commelin (Nov 18 2022 at 16:44):

Which is a similar pattern.

Eric Wieser (Nov 18 2022 at 16:44):

Johan, I think you're misreading structure wrap := (t : Type) for structure wrap := (val : some_type) where some_type : Type

Johan Commelin (Nov 18 2022 at 16:45):

Fair enough.

Mike Shulman (Nov 18 2022 at 18:58):

Well, the actual example has more fields of course:

structure group :=
  (t : Type)
  (op : t  t  t)
  -- etc.

Adam Topaz (Nov 18 2022 at 19:01):

You could probably @[derive has_repr] and save a few characters

Adam Topaz (Nov 18 2022 at 19:01):

(In the Nat case, that is)

Adam Topaz (Nov 18 2022 at 19:03):

What behaviour do you expect from eval in the group case?

Mike Shulman (Nov 18 2022 at 19:05):

group is the analogue of the general wrap. I would only want to display elements of particular groups, like a groupN.

Mike Shulman (Nov 18 2022 at 19:09):

Where do I put @[derive has_repr]?

Adam Topaz (Nov 18 2022 at 19:17):

hmmm derive doesn't quite work. sorry!

Mario Carneiro (Nov 18 2022 at 19:18):

wasn't the solution already shown?

instance : has_repr wrapN.t := nat.has_repr

Adam Topaz (Nov 18 2022 at 19:18):

yeah that works

Mario Carneiro (Nov 18 2022 at 19:24):

you can also do

instance : has_repr wrapN.t := by dunfold wrapN; apply_instance

if you don't know the instance name

Mike Shulman (Nov 18 2022 at 22:53):

Okay, this works for ℕ, but not for ℝ. When I try it with ℝ I get

kernel failed to type check declaration 't.has_repr' this is usually due to a buggy tactic or a bug in the builtin elaborator
elaborated type:
  has_repr Rvsp.t
elaborated value:
  id real.has_repr
nested exception message:
invalid definition, it uses untrusted declaration 'real.has_repr'

Eric Wieser (Nov 18 2022 at 22:54):

You need the word meta for real

Eric Wieser (Nov 18 2022 at 22:54):

Note that if you use my @[reducible] suggestion I made in the third post you don't have to deal with any of this

Mike Shulman (Nov 19 2022 at 01:58):

Where does the word meta go?

Adam Topaz (Nov 19 2022 at 02:02):

In the form meta instance ... should work

Mike Shulman (Nov 19 2022 at 02:17):

Thanks. What does meta mean?

Adam Topaz (Nov 19 2022 at 02:18):

It's a tag that's used for defs at the metaprogramming level

Adam Topaz (Nov 19 2022 at 02:19):

(In Lean3. Lean4 doesn't have meta.)

Mike Shulman (Nov 19 2022 at 02:20):

And why does the instance for real need to be at the metaprogramming level, but not the one for nat?

Adam Topaz (Nov 19 2022 at 02:21):

src#real.has_repr (just so I can take a look ;))

Mario Carneiro (Nov 19 2022 at 02:23):

I was wondering if you were going to ask that... :) It's the same issue I highlighted before: the implementation has to cheat using unsafe code to get at the representation behind the quotient

Mario Carneiro (Nov 19 2022 at 02:23):

The ultimate source of this unsafe hackery is src#quot.unquot

Mario Carneiro (Nov 19 2022 at 02:26):

As you yourself said @Mike Shulman there are no computable functions definable in the logic which can distinguish real numbers by a continuity argument, but clearly a function that turns a real into a string would have to do just that

Mario Carneiro (Nov 19 2022 at 02:30):

meta means "I don't care if this introduces type unsafety or unsoundness" and enables access to stuff like unchecked type casting, unguarded recursion and C++ FFI. The lean 4 equivalent is unsafe and luckily it is much less necessary than it was in lean 3. meta declarations don't exist as far as the kernel is concerned, they are only for the VM/compiler.

Mike Shulman (Nov 19 2022 at 02:33):

Thanks. I think the error message could have been more helpful in indicating that this was the problem...

Mario Carneiro (Nov 19 2022 at 02:34):

do you have a mwe?

Mario Carneiro (Nov 19 2022 at 02:34):

it is true that the error message is pretty bad, it looks like something made it past the first line of defense and you are getting the backup error message

Mike Shulman (Nov 19 2022 at 02:35):

import data.real.basic
structure wrap := (t : Type)
def wrapR : wrap := {t := }
instance : has_repr wrapR.t := by dunfold wrapR; apply_instance

Mario Carneiro (Nov 19 2022 at 02:39):

Huh, I guess that's always what you get when you use a meta declaration in a non-meta one.

meta def bar :  := 0
def foo :  := bar
-- kernel failed to type check declaration 'foo' this is usually due to a buggy tactic or a bug in the builtin elaborator
-- elaborated type:
--   ℕ
-- elaborated value:
--   bar
-- nested exception message:
-- invalid definition, it uses untrusted declaration 'bar'

The error for missing noncomputable is much better:

noncomputable! def bar :  := 0
def foo :  := bar
-- missing 'noncomputable' modifier, definition 'foo' depends on 'bar'

Mike Shulman (Nov 19 2022 at 03:59):

The last line "invalid definition, it uses untrusted declaration 'bar'" would be fairly informative if it were on its own.

Johan Commelin (Nov 19 2022 at 07:13):

Is this related to bundled?


Last updated: Dec 20 2023 at 11:08 UTC