The Stack Overflow podcast is back! Listen to an interview with our new CEO.

Questions tagged [type-inference]

The tag has no usage guidance.

66 questions
Filter by
Sorted by
Tagged with
28 views

Inferring the type of (f .) in Haskell

If we have the following in Haskell: f x y = x + y :type f f :: Num a => a -> a -> a then GHC would report ...
36 views

Real world example of contraction and weakening

Can you provide me a real world example of contraction and weakening in the type system of a popular language like Java, Kotlin, etc.? I heard that Rust has got explicit contraction but I don´t ...
69 views

Type inference for System F-omega

There have been some nice papers about simple type inference for System F: "HMF: Simple Type Inference for First-Class Polymorphism", "Practical type inference for arbitrary-rank types", and "Complete ...
150 views

Proving that the failure of algorithm W implies that the program is not typable

How one does prove that if algorithm W failed for a given program $e$ and context $\Gamma$, then there is no substitution $S$ and type $\tau$ such that $S\Gamma \vdash e : \tau$ ? The original paper ...
26 views

Is the expression (λx.xx)(λy.y) typeable in the following system?

We are given a simple functional language: $e ::= x | n | e_{1}e_{2}|\lambda(x:\tau).e$ with types: $\tau ::= \text{int} | \tau_{1} \rightarrow \tau_{2}| \tau_{1} \land \tau_{2}$ Is the ...
50 views

Is it possible to write a fully-decidable type system for the J language?

I'm experimenting with the J array language, a dynamically-typed array language with mutable assignment, subtyping, and function overloading (just like traditional APL). It is unclear to me whether ...
81 views

How does a compiler infer a value's type?

From A Swift Tour — The Swift Programming Language (Swift 5): var myVariable = 42 myVariable = 50 let myConstant = 42 A constant or variable must have the same ...
34 views

Add type checking/inference to my programming language

I am currently creating my own compiled programming language, and I have come to a point where I would like to start working on the type system and introduce some type checking. Ideally I would like ...
35 views

Projection operator for constraints

I was looking at HM(X) framework, Hindley-Milner parameterized by a constraint system X, and I was struggling to understand what does the projection operator $\exists \alpha$ does for a constraint. ...