# Tag Info

59

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 that they do this task methodically: if this number is greater than 9, then add a carry, and so forth. This description they just gave of what to do that is an ...

19

First, some remarks. Using only the core typed lambda calculus it's not possible to obtain 'a -> 'b because the typing system is in correspondence (via the Curry Howard isomorphism) to intuitionistic logics, and the corresponding formula A → B is not a tautology. Other extensions such as tuples and matchings/conditionals still preserve some logic ...

18

The skeleton is let f x = BODY. In BODY you must use x only in generic ways (for example, don't send it to a function that expects integers), and you must return a value of any other type. But how can the latter part be true? The only way to satisfy the statement "for all types 'b, the returned value is a value of type 'b" is to make sure the function does ...

18

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. For example, if you edit a Word document and press a key, the computer will show the letter you pressed. That's because a programmer wrote a program saying: If ...

16

In the lambda calculus with no constants with the Hindley-Milner type system, you cannot get any such types where the result of a function is an unresolved type variable. All type variables have to have an “origin” somewhere. For example, the there is no term of type $\forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta$, but there is a term of type $\... 12 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'll find instructions like this, taken word for word from Grandma's Polish Perogies: To cook perogies: Bring a large pot of lightly salted water to a boil. ... 10 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 symbols, $$\frac{\Gamma\vdash E:S\qquad S<:T}{\Gamma\vdash E : T}$$ The key thing here (and the reason I reviewed it) is that the same expression is given two ... 7 This is entirely dependent on the language, and even on the implementation. The type would typically include entries for primitive functions, external library bindings (e.g. file handles), byte-compiled functions, etc. in addition to the data types of the language. You can see a type like this in an interpreter for a dynamically-typed language written in a ... 7 Since you asked on a computer science site, I'll give you a computer science answer. This might not be the most directly helpful from a programmer's point of view, though understanding this will definitely make you a better programmer. The first argument to the printf function is a char *, i.e. a pointer to a byte¹. However, not all pointers to bytes are ... 7 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 code written in a programming language by a programmer. So if, for instance, we want the TV channel to change when we press a button, then we would need to write ... 7 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 help form our own thoughts. The Sapir-Whorf hypothesis says that the language that you use influences your thought. (The degree to which the Sapir-Whorf ... 6 Well, something known as parametricity tells us that if we consider the pure subset of ML (that is, no infinite recursion, ref and all that weird stuff), there is no way to define a function with this type other than the one returning the empty list. This all started with Wadler's paper “Theorems for free!”. This paper, basically, tells us two things: If ... 6 I suspect that this is intimately related to shadowing of fields in Java. When writing a derived class, I can, as in your example, write a field x that shadows the definition of x in the base class. This means that in the derived class, the original definition is no longer accessible via name x. The reason Java allows this is so that derived class ... 6 If all you have this definition rule (which doesn't perform any computation), it won't help you. You also need a way to use this definition, like you did in your code example: you implicitly used another language construct, where a definition is available in the next line. To make things precise, I'll consider a construct which combines a definition with a ... 6 Yes, you are restricting it too much. The second code is perfectly fine. For the record, Haskell has no issue with your code: > let myid = (\x->x)(\x->x) in (myid 'a', myid True) ('a',True) and Ocaml as well works fine, after eta-expansion: let myid y = (fun x -> x)(fun x -> x) y in (myid 'a', myid true);; - : char * bool = ('a', true) ... 5 The problem is that whatever the context$\Gamma$may imply about the variable$x$is irrelevant. This rule is intended to type a$\lambda$-abstraction, and the variable$x$may be changed to another variable by$\alpha$-conversion, without changing the semantics of the$\lambda$-abstraction, and thus without changing its type. By writing$\Gamma, x: \...

5

Java Bytecode Similar to Microsoft's CLS, the Java Bytecode that the Java virtual machine executes gives you the (theoretical) possibility of using libraries from one JVM-targeting language with another JVM-targeting language. For example, Java libraries can be used in Scala, which IMO is a much better language than Java itself. Libraries written in Scala ...

5

Your intuition that $\forall X.\, P(X)$ should be embeddable in $\exists X.\, P(X)$ is generally right. It only fails if the entire collection of types is empty, which is rarely the case. However, the specific example you gave $\forall X.\, (X \times (X \to Bool))$ is not a good one. A value of this type should be able to produce an element of every type $... 5 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. As we are dealing with an application, the only rule that applies is T-App, so we end up with the following (partial) typing derivation, where$\gamma$is yet ... 4 Let's get back to simpler objects: you cannot build an proper object of type 'a because then it would mean this object x can be used wherever 'a would fit. And that means everywhere: as an integer, an array, even a function. For example that would mean you can do things like x+2, x.(1) and (x 5). Types exist exactly to prevent this. This the same idea that ... 4 I would suggest first solving the all-pairs shortest distance problem on the graph$T$(or at least the single source version for each$p_i$as the source) using standard approaches. Then, for each function signature$F_j=f_1,\dots,f_n$, compute$\sum_{i=1}^nd(p_i,f_i)$, where$d(p,f)$is the distance between$p$and$f$(which can be infinite if$f$is not ... 4 This is a common limitation of type inferencing and it has to do with the distinction between parameters and results of a function. Generally type inferencing is done strictly with the parameters passed to a function. Consider just the expression: ImmutableMap.builder().build(); This has to be a valid expression due to how the language works. This means ... 4 Dependent Types in Racket are being worked on by Andrew Kent at Indiana University. There is a set of slides. There is a talk. Of interest, this potentially also impacts Typed Clojure, which is strongly modeled on Typed Racket. 4 As mentioned in the comments, it is possible to reduce simply typed lambda calculus to untyped lambda calculus. This is the approach associated with Alonzo Church, called "Church Types" or "intrinsic types". Here, types are embedded in the language, and are intrinsic to the language. Still, the language can be stripped of it's types. However, it is also ... 4 In Java, there is no 'static type of an object' - there is the type of the object, and there is the type of the reference. All Java methods are 'virtual' (to use C++ terminology), i.e. they are resolved based on the object's type. And btw. '@Override' has no effect whatsoever on the compiled code - it is just a safeguard that generates a compiler error if ... 4 Part of your intuition is correct: "terms" really means "the collection of terms generated thus far". I think you will also find in Pierce a definition that makes this explicit on the next page (Definition 3.2.3). What Pierce is actually doing is giving three equivalent and common ways of presenting syntax. In fact, the first one (page 24) is what you often ... 4 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 distinction between type inference, and the execution. The former happens strictly before the latter. BTW, it's wrong to say that an "interpreter does the jobs ... 4 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 Types and Programming Languages textbook by Benjamin Pierce as a general reference for this sort of thing. In there you can look up parametric polymorphism and ... 4 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 you say "my implementation happily infers the types of the above two functions to be ...". What functions? Functions are terms like (in this case)$\tt fun(x:...

4

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 types. In statically typed languages, variables do have types. Most modern statically typed general purpose languages have a form of type inference that can at ...

Only top voted, non community-wiki answers of a minimum length are eligible