Zulip Chat Archive

Stream: new members

Topic: Using dot notation on type aliases

Philipp (Dec 10 2023 at 19:11):

I want to define a type Pos storing x and y coordinates. To keep things simple I just use def Pos := Int × Int.

I can then define functions like

def Pos.valid (pos : Pos) : Bool :=
  pos.1  0 && pos.2  0

But how can I call them?

#eval (0,1).isValid
#eval ((0,1) : Pos).isValid

Results in

invalid field 'isValid', the environment does not contain 'Prod.isValid'
  (0, 1)
has type
  ?m.6156 × ?m.6164

It works if I introduce a let:

#eval let (p : Pos) := ((0:Int),(1:Int))

but that's not very convenient.

Philipp (Dec 10 2023 at 19:23):

Also, why would Pos not be inhabited? Am I using type aliases completely wrong?

Yaël Dillies (Dec 10 2023 at 19:24):

Yes. Type aliases forget a lot of things about the original type.

Yaël Dillies (Dec 10 2023 at 19:25):

For one, if you want to copy over an existing instance, you should use a deriving clause:

def Pos := Int × Int
deriving Inhabited

Kyle Miller (Dec 10 2023 at 19:28):

If you use abbrev Pos instead of def Pos then all instances and dot notation carry over

Last updated: Dec 20 2023 at 11:08 UTC