upvote

points

by antonvs23 hours ago |
comments
upvoteby rramadass13 hours ago|
next
[-]
To clarify further;

In "Simply Typed Lambda Calculus" (STLC) there are two grammars for a legal expression.

1) Type Grammar - Type ::= inbuilt types | Type1->Type2 (function)

2) Term Grammar - Term ::= constant | variable | lambda abstraction : "Type" | lambda application.

Note how in (2) above "Type" comes into the picture. During compilation, the expression's structure is analyzed and verified against the Typing Rules aka "Type Checking". Once this is passed the expression is considered sound and can be evaluated at runtime.

In "Calculus of Constructions" (CoC) the two grammars are unified into one which gives us powerful concepts like dependent types, polymorphism etc. - https://news.ycombinator.com/item?id=50137880

reply
upvoteby LoganDark23 hours ago|
prev|
[-]
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? :)

reply
upvoteby hexasquid22 hours ago|
parent|
next
[-]
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.

reply
upvoteby antonvs10 hours ago|
parent|
prev|
[-]
> Do you mean that if types had only to do with values, you would have to evaluate the term to determine type?

Exactly. And if that were the case, you couldn't do very much type checking at compile time.

Javascript, or more specifically Typescript, is precisely why I wrote "In most statically typed languages..."

In Typescript, you can write `1 + "hello"` and the type system will infer that the type of that term is 'string'. It doesn't change anything I wrote above.

reply