Remix.run Logo
▲ rramadass an hour ago

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