59
votes
Accepted
How can I explain to my parents that I study programming languages?
If you have a few minutes, most people know how to add and multiply two three-digit numbers on paper. Ask them to do that, (or to admit that they could, if they had to) and ask them to acknowledge ...
- 4,292
19
votes
How can I explain to my parents that I study programming languages?
I would try something like this:
Programmers can tell computers what to do. To do that, they need to use a programming language. That is a language that is understood by both computers and humans. ...
- 404
13
votes
What are the major differences between row polymorphism and subtyping
Subtyping says given an expression of one type we can give it also another type. We say the former is a subtype of the latter and this subtyping relationship induces many other relationships. In ...
- 12.1k
12
votes
How can I explain to my parents that I study programming languages?
Most people understand recipes. If you follow the instructions, you'll get a decent meal. Sometimes, though, the instructions can be difficult to follow. For example, when you're making perogies, you'...
- 423
8
votes
How can I explain to my parents that I study programming languages?
Your best bet may be to form analogies with human languages.
Programming languages are used to provide instructions to computers. Human languages are used to communicate ideas to other people and to ...
- 1,012
7
votes
How can I explain to my parents that I study programming languages?
Here is how I would (try) to explain this to my mom:
Programming languages are used by people to provide instructions to a computer. Everything that a computer does is done through some computer ...
- 71
6
votes
Accepted
In Hindley-Milner system, how can I prove that let id=\x.x in id id is well-typed?
If I understand you question correctly, you are wondering how the typing judgment $f : \forall \alpha. \alpha \to \alpha \vdash f\;f : \beta$ can be proved, where $\beta$ is some (yet unknown) type.
...
- 794
6
votes
Accepted
Polymorphism restriction on lambda-bound variables in HM
Yes, you are restricting it too much. The second code is perfectly fine.
For the record, Haskell has no issue with your code:
...
- 14.6k
4
votes
Accepted
Lambda Calculus Type Inference
Let me assume that you are asking about basic type inference for $\lambda$-calculus with parametric polymorphism a la Hindley-Milner (it's not entirely clear from your question). I would recommend the ...
- 30.4k
4
votes
Is type inference done by an interpreter static or dynamic?
Typically , type inference in interpreted languages happens after parsing (because type inference works on ASTs) but before interpretation (= execution). Both compilers and interpreters have a phase ...
- 8,308
4
votes
In Hindley-Milner system, how can I prove that let id=\x.x in id id is well-typed?
As a starting note, the rules are syntax-directed: there's only one rule for each language construct. This means that you can construct the typing proof from the bottom up, by always using the rule ...
4
votes
Accepted
Local type argument synthesis when type variable does not appear in arguments
As a prelude, there is some terminological confusion in your question. The issue is about a type variable occurring in a result type of a function. This is fairly minor. A more serious one is when ...
- 12.1k
4
votes
Accepted
Typing by value
Determining the type of a variable from the type of the value that is assigned to it is a form of type inference.
In dynamically typed languages, variables usually don't have types, only values have ...
4
votes
How does a language abstract away from underlying byte machines?
I'm assuming you are really asking
how is it possible that the same source code can be compiled to different architectures?
In order to achieve this feat different systems use different ...
- 1,080
3
votes
What is a type definition?
From "The C++ Programming Language" -by Bjarne Stroustrup the creator of C++.
A type defines a set of possible values and a set of operations (for
an object).
Also the following definitions are ...
- 131
3
votes
What is a type definition?
"Defining" a type is the act of building a new type composed of one or more pre-existing data types. For example, the "Complex Number" type is often declared as an ordered pair of "Real Numbers" :
<...
- 771
3
votes
How can I explain to my parents that I study programming languages?
You simply say "I am helping the guys who teach computers to work"
The idea is programmers teach computers to do stuff using programs and you are helping them. I think it will work assuming they ...
- 131
3
votes
How can I explain to my parents that I study programming languages?
computer languages relate somewhat roughly to human languages. they use standard/ common/ shared words. consider that there are thousands of human languages, some defunct, others active, and their ...
- 11k
3
votes
Accepted
What concept is for a name referring to different types at different points in execution?
A couple of things would fit the bill: polymorphism and dynamic typing.
Polymorphism
Say you have a polymorphic function, first:
...
- 200
3
votes
Accepted
Identification and the definition of data type
Is the use of identifiers then just a convenience for the programmer? In principle, couldn't you just replace the identifier with the type definition each time it was needed?
Yes. You can have a ...
- 29.8k
3
votes
How can I explain to my parents that I study programming languages?
Here are two analogies that you may find useful:
My work is somewhat like exploring new approaches to musical notation. (example) Although the predominant notation systems are quite sophisticated, it ...
- 666
3
votes
How can I explain to my parents that I study programming languages?
If you don't want to use comparisons, although I think the "algorithm" one that Lieuwe brought up is very nice to convey the idea, you could say that you want to reduce misunderstandings between ...
- 131
3
votes
Accepted
Typing rule for binding groups
I don't know what rule Jones intended to use, but I'd guess it's something like
$$
\dfrac{
\Gamma' = \Gamma,x_1:\tau_1,\ldots,x_n:\tau_n
\\
\Gamma' \vdash e_1 : \tau_1
\\
\cdots
\\
\Gamma' \vdash e_n ...
- 14.6k
2
votes
How can I explain to my parents that I study programming languages?
Well, most likely, you have some reason for studying languages - use that reason. E.g.:
I'm trying to make computers and their applications cheaper, easier to use and safer.
If that's something ...
- 181
2
votes
ML functions from polymorphic lists to polymorphic lists
Parametricity Theorem from the “Theorems for Free!” paper tells us that ML terms have a very special property: if we view a term’s type as a relation on values of this type, then this term’s value ...
- 245
2
votes
Accepted
Union of fixed and floating point types
Fixed (Qa.x) $\cup$ Float (FbEy) can be represented as Float (FcEz) where $c = a+x$ and $z = \max(\lceil \lg(x) \rceil,y)$. This is significantly more efficient than what you propose in the question....
D.W.♦
- 159k
2
votes
Union of fixed and floating point types
I actually think the simplest scheme would just to prepend a signal bit that says that the rest of the bits are either a floating point or fixed point value.
This always comes with a fixed cost of 1 ...
- 13.4k
2
votes
How is type safety handled differently between reference and value types?
There usually is metadata about the runtime class of an object contained within the object itself, regardless of what language you're working in. This metadata is essential in languages like C# that ...
- 262
2
votes
Accepted
Find typing derivation of STLC term with reference types
The expression $t$ does not contain any free variables, so one can start typing it with an empty context: $\emptyset\,|\,\Sigma~\vdash~t : \mathrm{Int}$, and attempt to build the full derivation tree ...
- 801
2
votes
What is "invariants of the code"?
An invariant is a statement that holds during the execution of a piece a code. For instance, you might often encounter loop invariants (statements that hold on every iteration of some loop) or class ...
- 22.6k
Only top scored, non community-wiki answers of a minimum length are eligible