Questions tagged [type-inference]
The type-inference tag has no usage guidance.
90
questions
0
votes
0
answers
31
views
Completeness of bidirectional type checking by inversion
I'm currently reading through the completeness proof of the paper "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism" by Dunfield et al.
In the second case Dunfield ...
8
votes
0
answers
73
views
When does type inference become undecidable in typed lambda calculus?
To begin with, if I understand correctly, in a simply typed lambda calculus, typing, type checking and type inference are always decidable. In the "full-fledged" polymorphic (terms depend on ...
- 109
0
votes
0
answers
65
views
Is type inference for arbitrary-rank types decidable when supplied type signatures?
I found following statements in 6.4.16. Arbitrary-rank polymorphism of ghc document.
GHC uses an algorithm proposed by Odersky and Laufer (“Putting type annotations to work”, POPL‘96) to get a ...
- 13
0
votes
0
answers
29
views
What is the general flow of the type inference algorithm in these cases where there is very little type information?
For a state of the art compiler, can they successfully do type inference on all of these cases, or are there some in which they can't? If there is a place which collects a bunch of test cases which a ...
- 2,265
0
votes
1
answer
127
views
How to think about typing inference rules when thinking about typechecking?
I am trying to build an imperative programming language with a type system that will allow for proofs. I just found kind lang, which implements all the ideas that I have been meaning to use (plus more)...
- 2,265
4
votes
3
answers
419
views
What is the runtime/time complexity of Coq’s (Dependent) Type Inference?
I remember learning in a class that type inference is decidable but usually takes a long time (e.g. type inference in OCaml is EXPTIME).
I was wondering, since Coq allows programs/values themselves to ...
- 3,060
3
votes
0
answers
325
views
What is the runtime (time complexity) of Type Inference in Simply Typed Lambda Calculus?
I was told that the runtime of OCAML or Scala is EXPTIME - which seems really bad! However, since people use type inference (deciding the type of a term or program or expression) in practice - it must ...
- 3,060
2
votes
0
answers
79
views
Understanding least common generalization (or anti-unification) of types
I am learning how to extend a basic Hindley-Milner type system to support overloaded variables by following Geoffrey Seward Smith's dissertation.
The proposed type inference algorithm makes use of the ...
- 131
5
votes
1
answer
251
views
Free variables in constraint-typing derivation?
In Types and Programming Language's constraint typing rules (Figure 22-1), is it possible for any part of the typing derivation to contain free type variables that aren’t part of the fresh variables? ...
- 183
0
votes
0
answers
36
views
Is type unification a kind of search for alpha equivalence?
I was reading about type unification and it moves through of substitution of variables. To me it looks like a search for an alpha equivalence... I mean, two types are unifiable if they are alpha ...
- 243
4
votes
1
answer
98
views
Which language is used to construct a type system?
Typically, OCaml and Scala seem to be used for designing any programming languages tool. But what features offer them an edge over other languages.
A related question, is a type system for a language ...
- 43
0
votes
0
answers
43
views
RDF | If something is a rdfs:subClassOf of :Q can you infer it is also rdf:type :Q?
Given:
:P rdfs:subClassOf :Q
Can you infer the following?:
:P rdf:type :Q
I do not think you can, but I am not fully sure. ...
- 156
3
votes
1
answer
55
views
Annotated type system problem about conditional branch
I am reading the book "Principle of Program Analysis" by Flemming Nielson for annotated type systems. In the first chapter, section 1.6 they mentioned the simple type system for various ...
- 151
3
votes
1
answer
274
views
Curry-Howard, void, and type checking in Haskell
I am trying to understand an example of theorem proving via type checking in Haskell given here. The example is as follows.
Using the Curry-Howard isomorphism, construct an inhabitant of the type and ...
- 565
2
votes
1
answer
111
views
Type-checking function calls with functional subtyping
I'm relatively new to the topic. Suppose that you want to type-check an expression of the form f(a), i.e. a function call. Assuming that all the declarations are ...
- 183