> These are the constructs we manipulate in our programs, things like 1, 2, True, "hello", etc… In functional programming contexts, they're also called "terms."

This is not correct. Terms are syntactic expressions in a program. For example, 1+2 is a term, but it’s not a value. At runtime, it evaluates to 3. As such, some terms correspond directly to values - like 1 - but other terms represent computations that will be performed at runtime.

tl;dr: terms are a syntactic concept, values are a runtime concept. Terms evaluate to values.

▲

antonvs 5 hours ago | parent | next [-]

Following on from the above, this statement is also incomplete at best:

> Types are groups of related values.

This is an operational perspective which misses one of the most important aspects of types: in a statically typed language, types are a way to classify terms, i.e. they're not just about values.

As an example of why this distinction matters, consider this expression: 1 + "hello". In most statically typed languages, this will be rejected at compile time. It doesn't have to be evaluated (i.e. at runtime) to be rejected - it's invalid because the types of the terms - 1 and "hello" - aren't compatible.

This compile-time rejection is only possibly because types apply to terms, and terms aren't values. This is critical to the usefulness of statically-typed languages - without this, they'd have to run the program to detect type errors.

Benjamin Pierce's book "Types and Programming Languages" has some great coverage of this topic.

▲

LoganDark 4 hours ago | parent [-]

Do you mean that if types had only to do with values, you would have to evaluate the term to determine type?

Also, 1 + "hello" is "1hello", obviously. Have you never read JavaScript? :)

	▲	hexasquid 3 hours ago \| parent [-]
		I gather it goes through an intermediate coercion step where it is "1" + "hello". What trips us up is having existing expectations for what an operator called + should do.

▲

thaumasiotes 4 hours ago | parent | prev [-]

> This is not correct.

Why do you think so? It's a completely standard usage. For example, we can ask MathWorld:

> In logic, a term is a variable ['a', 'f'], constant ['1', '"hello"'], or the result of acting on variables and constants by function symbols ['1+2', 'f(a)'].

(I've added the bracketed material, which provides examples of the senses that MathWorld gives. https://mathworld.wolfram.com/Term.html )

In particular, note that by this wording, if you're looking at '1+2', the "term" is not the string '"1+2"' but the result of adding '1' to '2', which is '3'.

You can talk about 'terms' in the context of how a compiler views source code. Or you can talk about 'terms' in the context of how type theory applies to some computation. They'll be called 'terms' either way; you seem to have staked out the position that the compiler context is obligatory and the type theory context is somehow in error.

	▲	rramadass 16 minutes ago \| parent [-]
		Terms are a syntactic concept while Values are a semantic runtime concept. The key to understanding is that Values are Terms which have been reduced (i.e. evaluated) to normal form and hence cannot be reduced further. The nuance lies in the fact that while both unreduced Terms and reduced Values can have semantic meanings, only at the Value stage is it canonical and fully computed. In fact the "Calculus of Constructions" (CoC) derived from Typed Lambda Calculus unifies everything into a Term like so; Term ::= variable \| lambda abstraction \| lambda application \| dependant product \| sorts (type of types) For reference see Brandl's work that i list here - https://news.ycombinator.com/item?id=50028902