formal systems to specify properties of objects
2
votes
0answers
46 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 ...
4
votes
1answer
58 views
What is the difference between the semantic and syntactic views of function types?
Edit: My original question referred to nonconstructive and constructive definitions of function types. I changed the terminology in the question and the title to semantic and syntactic, which the ...
9
votes
2answers
211 views
How are programming languages and foundations of mathematics related?
Basically I am aware of three foundations for math
Set theory
Type theory
Category theory
So in what ways are programming languages and foundations of mathematics related?
EDIT
The original ...
4
votes
3answers
121 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
161 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 ...
3
votes
2answers
176 views
Why classes implicitly derive from only the Object Class?
I do not have any argument opposing why we need only a single universal class. However why not we have two universal classes, say an Object and an AntiObject Class. In nature and in science we find ...
6
votes
1answer
91 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:
...
11
votes
1answer
300 views
Does there exist a Turing complete typed lambda calculus?
Do there exist any Turing complete typed lambda calculi? If so, what are a few examples?
4
votes
2answers
140 views
What is the type theory judgement symbol?
In type theory judgements are often presented with the following syntax:
My question is what is that symbol in the middle called? All the papers I've found seem to use an image rather than a ...
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 ...
11
votes
3answers
295 views
Categorisation of type systems (strong/weak, dynamic/static)
In short: how are type systems categorised in academic contexts; particularly, where can I find reputable sources that make the distinctions between different sorts of type system clear?
In a sense ...
6
votes
3answers
270 views
How to read typing rules?
I started reading more and more language research papers. I find it very interesting and a good way to learn more about programming in general. However, there usually comes a section where I always ...
5
votes
3answers
211 views
Simple explanation as to why certain computable functions cannot be represented by a typed term?
Reading the paper An Introduction to the Lambda Calculus, I came across a paragraph I didn't really understand, on page 34 (my italics):
Within each of the two paradigms there are several versions ...
9
votes
1answer
139 views
Is there a typed SKI calculus?
Most of us know the correspondence between combinatory logic and lambda calculus. But I've never seen (maybe I haven't looked deep enough) the equivalent of "typed combinators", corresponding to the ...
10
votes
1answer
177 views
Constraint-based Type Inference with Algebraic Data
I am working on an expression based language of ML genealogy, so it naturally needs type inference >:)
Now, I am trying to extend a constraint-based solution to the problem of inferring types, based ...
8
votes
2answers
271 views
What is beta equivalence?
In the script I am currently reading on the lambda calculus, beta equivalence is defined as this:
The $\beta$-equivalence $\equiv_\beta$ is the smallest equivalence that contains ...
8
votes
2answers
250 views
Recursive definitions over an inductive type with nested components
Consider an inductive type which has some recursive occurrences in a nested, but strictly positive location. For example, trees with finite branching with nodes using a generic list data structure to ...
16
votes
2answers
171 views
Characterization of lambda-terms that have union types
Many textbooks cover intersection types in the lambda-calculus. The typing rules for intersection can be defined as follows (on top of the simply typed lambda-calculus with subtyping):
$$
...
11
votes
2answers
166 views
Are universal types a sub-type, or special case, of existential types?
I would like to know whether a universally-quantified type $T_a$: $$T_a = \forall X: \left\{ a\in X,f:X→\{T, F\} \right\}$$ is a sub-type, or special case, of an existentially-quantified type $T_e$ ...
