The tag has no wiki summary.

learn more… | top users | synonyms

10
votes
1answer
177 views

What are the practical issues with intersection and union types?

I'm designing a simple statically typed functional programming language as a learning experience. It appears that the type system I have implemented so far could (with a little extra work) ...
9
votes
1answer
158 views

A simple proof that decidability of typability in System F ($\lambda 2$) implies decidability of type checking?

Suppose we don't know Joe B. Wells's result from 1994 that both typability and type checking are undecidable in System F (AKA $\lambda 2$). In Barendregt's Lambda calculi with types (1992) I found a ...
1
vote
1answer
107 views

How to generalize a map of type for many operators?

I am formalizing the type system for a small language, and thus writing inference rules. Taking unary - operator for example, its entry may be a number as well as ...
9
votes
2answers
233 views

Research on call-site based type inference?

I'm trying to learn more about whole-program type checking and type inferencing systems that use information from function call sites to compute type information (in addition to the standard approach ...
8
votes
2answers
905 views

Type inference for imperative statements other than assignment

In my search for research papers about type systems for imperative languages, I only find solutions for a language with mutable references but without genuine imperative control structures such as ...
6
votes
1answer
260 views

What is the role of the Bicolored Calculus of Constructions?

So, I'm reading a bit about elaboration, particularly, algorithms based on the Bicolored Calculus of Construction, and I'm a bit confused. I don't understand what exactly the purpose of the $CC^{bi}$ ...
5
votes
2answers
346 views

the type system does not tell the whole story due to “exception”

I am wondering whether it is a bad style to use "exception". For example, in Ocaml, the exception does not appear as the .mli file. So it appears to me that "exception" is something that cannot be ...
6
votes
1answer
275 views

Implications of the rule of cumulativity in the Calculus of Constructions

Please help me understand some type theory research. As suggested in "Type Checking with Universes" by Robert Harper and Robert Pollack, we can add the following rule to our otherwise standard COC or ...
5
votes
2answers
268 views

With equirecursive types are there downsides to making all types potentially recursive?

By this I mean to ask, is it a bad idea to have all type constructor term expressions abstracted with $\mu$ just in case they need to be recursive? For example, $Bool : Type;$ $Bool = (\mu Bool' ...
21
votes
2answers
939 views

Context Sensitive Grammars and Types

1) What, if any, is the relationship between static typing and formal grammars? 2) In particular, would it be possible for a linear bounded automaton to check whether, say, a C++ or SML program was ...
5
votes
1answer
151 views

Nested automatization of type inference of forall elimination

Following a previous question about how to automatize the type inference in a forall elimination of an application, now suppose we want to do the same but for a nested forall, say $(\Lambda ...
9
votes
1answer
284 views

In System F à la Church, can we automatize type inference for the for-all elimination?

The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$. Now, suppose ...
7
votes
0answers
245 views

Type inference with subtype constraints and polymorphism using Trifonov and Smith's constraint maps

Trifonov and Smith's Subtyping Constrained Types (1996) introduces constraint maps to represent consistent closed constraint sets (such maps providing sets of lower and upper bounds to each variable ...