Looking for the right expression

Stream: new members

[Leandro Caniglia]

If I have

structure TPoint (τ : Type) where
  x : τ
  y : τ
deriving Repr

then I can write

def nw : TPoint Int := {x := -1, y := 1}
#eval nw

My question is what expression should I #eval to get the TPoint Int with coordinates -1 and 1? I've tried several combinations and none worked. Among them, #eval TPoint.mk Int (-1) 1.

[Kyle Miller]

Here's an option:

#eval {x := -1, y := 1 : TPoint Int}

[Leandro Caniglia]

Kyle Miller said:

#eval {x := -1, y := 1 : TPoint Int}

Thanks!

[Leandro Caniglia]

My follow up question would be whether we have some form of mk for TPoint Int.

[Kyle Miller]

You should be able to write (TPoint.mk (-1) 1 : TPoint Int). Or, you could probably do @TPoint.mk Int (-1) 1

[Leandro Caniglia]

Kyle Miller said:

TPoint.mk (-1) 1 : TPoint Int

I see. Those are the expressions I was trying to find. Thanks again.

[Mark Fischer]

@Kyle Miller Are the parameters to a structure (so in this case τ : Type) always implicit values in the constructor? It looks like this compiles fine:

structure TPoint {τ : Type} where
  x : τ
  y : τ
deriving Repr

Is there a difference in this case?

---

@Leandro Caniglia As an aside, the following works for me too:

#eval TPoint.mk (-1 : Int) 1

[Leandro Caniglia]

Treq said:

#eval TPoint.mk (-1 : Int) 1

Interestingly, #eval TPoint.mk (-1) 1 also works. It looks like there is some sort of type inference in place and we don't need to specify it. However, #eval TPoint.mk 1 1 would infer τ to be Nat, which might not be the desired type.

What I don't understand is why #eval TPoint.mk Int 1 1 doesn't work. I find it quite confusing.

[Kyle Miller]

Do you understand implicit vs explicit arguments? Take a look at #check TPoint.mk (or hover over TPoint.mk) to see which arguments are explicit and which are explicit.

[Kyle Miller]

@Treq Parameters are always implicit for each of the projections, so making it implicit makes no difference there, but generally structure TPoint {τ : Type} where is not a good idea because then you can almost never write TPoint by itself for the type. You need to write @TPoint Int or TPoint (τ := Int) .

[Leandro Caniglia]

Kyle Miller said:

Do you understand implicit vs explicit arguments?

Not yet. However, after you suggestion I tried #eval TPoint.mk (τ := Int) 3 4 and I got the intended TPoint Int. I guess this will get clearer as I progress in the book.

[Kyle Miller]

Curly brace arguments (implicit arguments) are not passed to functions explicitly, and they're meant to be inferred from the other arguments, or from the return type itself. In functions, most commonly they're used for type parameters.

[Mark Fischer]

I suppose the final detail to add here is that implicit arguments can be given explicitly by either using @ before a function call or passing it as a named parameter. Hense @TPoint.mk ℤ or TPoint.mk (τ := ℤ)

[Leandro Caniglia]

Mark Fischer said:

Hence @TPoint.mk ℤ or TPoint.mk (τ := ℤ)

This is a useful clarification to my question. Thanks.