Fields with Types implementing classes

Stream: new members

[Luis Enrique Muñoz Martín]

Hi, why do the following field1 and field2 have different underlying types?

structure Ty where
  Field1 : Type
  Field2 {X : Type} : X

def foo : Ty := {
  Field1 := Int // Works fine
  Field2 := Int // Doesn't works <--
}

Ideally I would want the second field to work to be able to make something like:

structure Config where
  Number {X : Type} [Add X] : X
  -- Other types with other classes

def myConfig : Config := {
  Number := Nat
  -- Number := String  will not compile
}

[Yaël Dillies]

Field2 {X : Type} : X means "For every type X, an element of X", while Field1 : Type means "A type"

[Yaël Dillies]

In other words, Field2 is a function which chooses an element of every type. Such a function does not exist, since empty types (eg Empty or False or Fin 0) exist

[Yaël Dillies]

I think what you want is rather

structure Config where
  Number : Type
  add : Add Number

[Eric Wieser]

Or even [add : Add Number] which will make filing it automatic

[Luis Enrique Muñoz Martín]

Technically speaking if

Field2 {X : Type} : X means "For every type X, an element of X"

then increasing the universe Field2 {X : Type 1} : X, X should be the type I used later to configure it? (Int)

The compiler doesn't work with it, but both sides looks pretty similar:

has type
  Type : Type 1
but is expected to have type
  X✝ : Type 1

[Daniel Weber]

What do you mean? This?

structure Config where
  Field2 {X : Type 1} : X

Note that this is still an empty type -

example (c : Config) : False := PEmpty.elim c.Field2

[Luis Enrique Muñoz Martín]

Yes, I meant that.

With empty type, you mean it's impossible to initialize Field2 with any existent type, right?

[Daniel Weber]

I mean that there's no object of type Config