Opaque type with interface

Stream: lean4

[Marcus Rossel]

Is it possible to define an opaque type (via constant) about which some properties are known?
E.g. if I want to say that Value is a type and it should be the case that x is a value of type Value, I would start with:

constant Value: Type _
constant x : Value

Now Lean complains: failed to synthesize Inhabited Value
Since we know nothing about Value, there isn't any sensible way to define x manually either.

Is there some way to make this setup work though?

[Henrik Böving]

Via an axiom.

[Marcus Rossel]

Henrik Böving said:

Via an axiom.

Mhh yeah, I was afraid that would be the only way.

[Henrik Böving]

Do you have a concrete example from your project? Maybe we can get that to work without an axiom

[Marcus Rossel]

In the spirit of #xy, the reason why I'm asking is the following:
I have a Thing type that acts on instances of some Value type. What the concrete Value type is doesn't really matter though, I only need to know that it has an element x. So currently I model Value as a type parameter (with the appropriate type class constraint):

class ValueType (Value : Type _) where
  x : Value

struct Thing (Value : Type _) [ValueType Value] where
  doThing: Nat -> Value

This is kind of annoying, because throughout the entire project, I never care what Value is, so I always have to use Thing with an additional variable:

variable (Value : Type _) [ValueType Value]

def f (t : Thing Value) : Thing Value := ...

I'd like to somehow state once that Value is just some type that fulfils certain requirements and that Thing uses that type (without being specific about what Value is).

[Henrik Böving]

First things first you can get rid of your ValueType, it's equivalent to Inhabited...but if you need access to some arbitrary value of your generic type there will be no prettier way than the Inhabited typeclass I know of.

[Marcus Rossel]

Henrik Böving said:

First things first you can get rid of your ValueType, it's equivalent to Inhabited...but if you need access to some arbitrary value of your generic type there will be no prettier way than the Inhabited typeclass I know of.

In my real world project it's more like a pointed type. The x is a value with a specific meaning.

[Reid Barton]

For your original question you can make a constant of type "type together with an element of the type" and then unpack that into two definitions Value and x.

[Reid Barton]

I'm more confused by the longer explanation though--if you don't care what Value is then why not just use Unit? if you do care then why would it make sense to use constant, or not express the dependence of Thing on it?

[Marcus Rossel]

Reid Barton said:

For your original question you can make a constant of type "type together with an element of the type" and then unpack that into two definitions Value and x.

Like this?: constant Value : Σ V : Type _, V

[Marcus Rossel]

Reid Barton said:

I'm more confused by the longer explanation though--if you don't care what Value is then why not just use Unit? if you do care then why would it make sense to use constant, or not express the dependence of Thing on it?

I don't want to use a concrete type (like Unit) so that I don't accidentally use any properties specific to that type in my construction.
The type parameter approach does exactly what I want, it's just unwieldy.

[Marcus Rossel]

I think I'm going to go with this now:

private constant _Value : Σ V : Type _, V := Sigma.mk Unit Unit.unit

def Value : Type _ := _Value.fst
constant Value.absent : Value := _Value.snd

struct Thing where
  doThing: Nat -> Value

Thanks for your help!

[Yakov Pechersky]

This looks like a job for typeclasses that have a single x record

[Yakov Pechersky]

You have concrete structures that are instances of that typeclass. And functions that don't care about the particular value are constrained to take in types that are instances of that typeclass

[Yakov Pechersky]

That typeclass is "like" declaring a scoped, namespaced axiom

[Marcus Rossel]

Yakov Pechersky said:

You have concrete structures that are instances of that typeclass. And functions that don't care about the particular value are constrained to take in types that are instances of that typeclass

Yes, that's what my project currently uses. But as previously mentioned, that has the annoying side effect that I can't just use Thing, but instead always have to use Thing Value.
(In my real project I have another type like Value, so its even worse: Thing Value Other)

[François G. Dorais]

This looks really similar to how floats are handled in core. There, Inhabited is justified by a trivial object (e.g. 0 or NaN, whatever). That's enough to make all partial definitions work. The value of the trivial object is totally irrelevant. However, as far as Lean theorem proving is concerned, all partial definitions might always return that value.

It's unusual that your Thing has no random value, that amounts to a useless type, which is something to complain about, I guess... Your Thing probably has some useless value that you can formalize in Lean!

[François G. Dorais]

From your last message, it seems that Thing might be a discriminated type where it either applies to Foo or Bar depending on whether it gets a Foo or a Bar. In that case, consider formalizing the discriminant but not the implementation.