type abbreviations

Stream: general

[Brian Milnes]

It's quite useful to have type abbreviations in a large PL model, are there any?

[Kevin Lacker]

ℕ is an abbreviation for nat, at least if you measure by number of unicode characters rather than general annoyance of typing

[Mario Carneiro]

There are lots of kinds of "abbreviation", with different use cases:

1. def type := other_type
2. @[reducible] def type := other_type

3. notation `type` := other_type

   • local notation `type` := other_type

4. abbreviation type := other_type

I usually recommend 1 or 3, rarely 2

[Mario Carneiro]

The one Kevin mentions is (3)

[Yakov Pechersky]

What's the downside of 4?

[Eric Wieser]

4 is 2 + @[inline], right? Does attr#inline have docs?

[Eric Wieser]

Seemingly not

[Mario Carneiro]

I don't think inline is related to any of these. That has to do with code evaluation, and types aren't evaluated in that sense anyway

[Mario Carneiro]

I just checked the code: abbreviation is indeed a synonym for @[inline, reducible] def

[Mario Carneiro]

I had thought it also included a kernel reducibility setting, but it doesn't look like it

[Mario Carneiro]

inline means what it does in most programming languages: the code for the definition is inlined into wherever it is used

[Mario Carneiro]

So to update my recommendations, I would suggest 4 in the same situations as 2 (@[inline] usually doesn't matter unless you are writing monad combinators)

[Mario Carneiro]

But I think that it's best not to use reducible defs when possible, because they can cause invisible blowups behind the scenes. If you make a definition, you should opt in to any type classes you want to inherit