The tag has no wiki summary.

learn more… | top users | synonyms

3
votes
1answer
51 views

Meaning of type inference rule for abstraction in lambda-calculus

Below is a snippet about simply typed lambda-calculus from CS152: Programming Languages Lecture 9 | Simply Typed Lambda Calculus, on printed‑page 15, indexed 23. $$ \frac {\Gamma, x: \tau_1 \vdash e: ...
4
votes
2answers
216 views

Why isn't the Swift programming language type inference more aggressive?

Couldn't the type inference in Apple's new programming language Swift had been done more aggressive? For instance why can't the return type of a function be deduced? ...
0
votes
0answers
21 views

Type inference example?

In my programming languages course we are reviewing type inference, i didnt get very well how to make this task. I all ready search at the bibliography of my course (PLAI by Shriram krishnamurthi) ...
0
votes
0answers
7 views

How to apply the unification algorithm to a racket function

In my programming languages course we are reviewing unification algorithm by hand. The TA can't solve some examples of how to apply the unification algorithm to the ...
3
votes
0answers
22 views

Is dependency analysis required in order to type a program?

I have seen stated in various places that in order to allow an "increase in polimorphism" functional depency analysis should be performed, and type inference should be used for every declaration group ...
5
votes
1answer
53 views

Type inference + overloading

I'm looking for a type inference algorithm for a language I'm developing, but I couldn't find one that suits my needs because they usually are either: à la Haskell, with polymorphism but no ad-hoc ...
3
votes
0answers
40 views

Does there exist a type system for a non-let-polymorphic lambda calculus?

I'm wondering if there is a way to extend Hinley-Milner's type system to allow polymorphic types without the need of a let construct, by adding an intersection type (as Dan pointed out) that ...
6
votes
2answers
176 views

Define a list using only the Hindley-Milner type system

I'm working on a small lambda calculus compiler that has a working Hindley-Milner type inference system and now also supports recursive let's (not in the linked code), which I understand should be ...
7
votes
1answer
129 views

Why will the Hindley-Milner algorithm never yield a type like t1 -> t2?

I'm reading about this algorithm while writing an implementation, and see that, as long as every variable is bound, you'll always get either atomic types or types where the arguments will determine ...
3
votes
1answer
53 views

Type inference of pair (product) types

I am looking into Hindler-Milney type system and I am trying to add support for the pair type. In Pierces book, he introduces special language constructs for creation of pairs and getting their ...
11
votes
1answer
517 views

What makes type inference for dependent types undecidable?

I have seen it mentioned that dependent type systems are not inferable, but are checkable. I was wondering if there is a simple explanation of why that is so, and whether or not there is there a limit ...
0
votes
1answer
96 views

Is constant a variable or subtype?

I think of type as a range of values that the variable can take whereas the rest is known constant or does not matter. Variables (instances or objects), which share common properties, are considered ...
2
votes
0answers
134 views

Encoding row types

I'm working on a type system with extensible records, similar to ones explained in "A Polymorphic Type System for Extensible Records and Variants - Benedict R. Gaster and Mark P. Jones" and ...
3
votes
1answer
69 views

ML - Type Interface

From my recitation class - Can you please explain why does operator $"+"$ signature is $ int \rightarrow (int \rightarrow int)$ ? How does this graph is build ? And what is mean $t=u ...
5
votes
3answers
287 views

How can SML infer types like this?

Wikipedia says: fun factorial n = if n = 0 then 1 else n * factorial (n-1) A Standard ML compiler is required to infer the static type int -> int of ...
8
votes
1answer
519 views

Concise example of exponential cost of ML type inference

It was brought to my attention that the cost of type inference in a functional language like OCaml can be very high. The claim is that there is a sequence of expressions such that for each expression ...
8
votes
1answer
158 views

Inferring refinement types

At work I’ve been tasked with inferring some type information about a dynamic language. I rewrite sequences of statements into nested let expressions, like so: ...
3
votes
1answer
196 views

Is the type inference here really complicated?

There's a question on SO asking why in Java the right type doesn't get picked in a concrete case. I know that Java can't do it in such "complicated" cases, but I'm asking myself WHY? The (for ...