verifying that a variable, expression or value has the declared type
0
votes
0answers
15 views
What is a preterm parser?
I am working with HOL-Light parser and keeping seeing references to preterm parser.
What is a preterm parser?
The most informative statement I find is from the HOL-Light reference for the ...
2
votes
0answers
47 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
39 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 ...
8
votes
1answer
166 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 ...
10
votes
1answer
190 views
Type inference with product types
I’m working on a compiler for a concatenative language and would like to add type inference support. I understand Hindley–Milner, but I’ve been learning the type theory as I go, so I’m unsure of how ...
7
votes
2answers
435 views
Type-checking algorithms
I am starting a personal bibliographic research on type-checking algorithms and want some tips. What are the most commonly used type-checking algorithms, strategies and general techniques?
I am ...
