Stream: t-compiler

Topic: Renaming `Kind`


RalfJ (Jul 19 2019 at 13:07, on Zulip):

Sorry, I was referring to the type theory notion of "kind", not the Kind in rustc... which we should already rename to Term or something (idk if there is a discussion somewhere).

This compiler type is, in type-theoretic terms, something like exists k: kind, thing_of_kind k. I would expect that a Kind would be defined as enum Kind { Lifetime, Type, Const }.

Should we rename the rustc thing to align the terms with type theory/PL? Or are there other contexts in which rustc's use of "kind" is correct?

RalfJ (Jul 19 2019 at 13:07, on Zulip):

@eddyb ^

RalfJ (Jul 19 2019 at 13:08, on Zulip):

I was not sure what to propose as a name, but "term" seems good -- way better than "kind", for sure

eddyb (Jul 19 2019 at 13:08, on Zulip):

yeah I just didn't know any better when I added Kind

eddyb (Jul 19 2019 at 13:09, on Zulip):

I think @varkor and/or @centril have seen this "Term" idea before but idk where the discussion was

varkor (Jul 19 2019 at 13:17, on Zulip):

the problem with "term" is that it usually refers to a term of a type, which is only one particular case here

varkor (Jul 19 2019 at 13:18, on Zulip):

maybe something longer like "KindTerm"

eddyb (Jul 19 2019 at 13:32, on Zulip):

eh

eddyb (Jul 19 2019 at 13:32, on Zulip):

in a good language Type is a term of type Type1 or w/e :P

eddyb (Jul 19 2019 at 13:33, on Zulip):

and so on and so forth

RalfJ (Jul 19 2019 at 15:02, on Zulip):

hm yeah I guess a term is usually something that has a type, whereas we are looking for a name for "something that has a kind"

eddyb (Jul 19 2019 at 15:03, on Zulip):

I hate that we even need this discussion Q_Q

eddyb (Jul 19 2019 at 15:03, on Zulip):

/me shakes fist at academia for not making this easier

eddyb (Jul 19 2019 at 15:04, on Zulip):

we could call it something dumb like LoToC or ToLoC

eddyb (Jul 19 2019 at 15:04, on Zulip):

"lifetime or type or const"

eddyb (Jul 19 2019 at 15:04, on Zulip):

"To" is ambiguous tho, maybe TorLorC is better

Tom Phinney (Jul 19 2019 at 15:05, on Zulip):

Or maybe give it a little love and call it "TLC"?

Tom Phinney (Jul 19 2019 at 15:07, on Zulip):

Guess I should have added an explanatory link for the acronym: https://dictionary.cambridge.org/us/dictionary/english/tlc

RalfJ (Jul 19 2019 at 15:20, on Zulip):

/me shakes fist at academia for not making this easier

academia shakes fist back -- naming is hard ;)

RalfJ (Jul 19 2019 at 15:21, on Zulip):

"KindedTerm" I think would be closer to how I would call this in a paper

eddyb (Jul 19 2019 at 15:37, on Zulip):

/me hmm, "kindled"

eddyb (Jul 19 2019 at 15:38, on Zulip):

more seriously, KindedTerm is fine with me :D

RalfJ (Jul 19 2019 at 15:39, on Zulip):

for any German speaker who's reading, I'd like to relay this one (when I asked elsewhere about this question):
"thing that has a kind" -- parent

RalfJ (Jul 19 2019 at 15:40, on Zulip):

For anyone else, here is a hint.

RalfJ (Jul 19 2019 at 15:55, on Zulip):

seems like there is some literature where this is called a "type expression"

RalfJ (Jul 19 2019 at 15:55, on Zulip):

but I somehow find that a strange term to use

eddyb (Jul 19 2019 at 16:17, on Zulip):

I've seen "expression" used to refer to the syntax used to create a "term"

eddyb (Jul 19 2019 at 16:17, on Zulip):

so a type expression would evaluate to a type term

eddyb (Jul 19 2019 at 16:17, on Zulip):

and terms are defined as values whereas expressions can compute (to reach a value)

eddyb (Jul 19 2019 at 16:18, on Zulip):

(but this might vary a lot between situations)

Last update: Nov 22 2019 at 04:35UTC