The type-systems tag has no wiki summary.
6
votes
1answer
112 views
Constraint types (IBM/X10) compared to dependent types
Constraint types have been proposed by IBM in their X10 programming language (it's a commercial programming language, not open source software).
Nystrom, Nathaniel, et al. "Constrained types for ...
0
votes
0answers
56 views
Semantics of a programming language [duplicate]
A newbie question, if I may... Could you be so kind and explain to me in plain english meaning of 'denotational semantics' and 'operational semantics'? I'm familiar with the definitions and have read ...
4
votes
0answers
89 views
Type-and-effect systems, stochasticism and effect squelching: how about quicksort?
There's a feature of Haskell's type system which bugs me: you can't implement a randomized sorting algorithm without the use of randomness spilling out into all of its callers. That seems ...
4
votes
0answers
146 views
Commonalities and differences between canonical structures and the implicit calculus
There is a paper on The Implicit Calculus as a generalization of type classes. Coq's canonical structures are also a generalization of type classes. The paper does not mention canonical structures ...
7
votes
2answers
463 views
Free theorems, where?
I've found this webapp which lets you generate a free theorem for a given type.
The generated theorems quantify over types and relations on these types. These theorems (formulas) are theorems of ...
1
vote
1answer
91 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 ...
10
votes
1answer
324 views
A mathematical (categorical) description of type classes
A functional language can be viewed as a category where its objects are types and morphisms functions between them.
How do type classes fit in this model?
I assume we should only consider those ...
9
votes
1answer
202 views
What are possible implementations of Haskell's type classes and what are their (dis)advantages?
As far as I know, a Haskell function with type classes constraints is internally compiled to a function with additional arguments that receive dictionaries with the necessary implementations of each ...
4
votes
1answer
185 views
Classes and types in object-oriented languages
In typical object-oriented programming languages like Java, classes are used as types. On the other hand, type-theoretic approaches to object-oriented languages treat interfaces as types.
Are there ...
9
votes
2answers
281 views
Ownership types and Separation Logic
Ownership types and Separation Logic seem to have similar goals, control over ownership and aliasing. Perhaps, I should also add: the ability to write modular specifications.
What is known about the ...
7
votes
1answer
224 views
Proofs techniques related to Curry–Howard correspondence
I am looking for sources about formalized notion of programs. This seems to be closely related to Curry-Howard correspondence, but one could also track this back to Universal Turing Machines and its ...
8
votes
4answers
344 views
Unary parametricity vs. binary parametricity
I've recently become quite interested in parametricity after seeing Bernardy and Moulin's 2012 LICS paper ( http://www.cse.chalmers.se/~mouling/share/AComputationalInterpretationOfParametricity.pdf). ...
3
votes
0answers
98 views
Forms of types in the calculus of constructions
In the usual presentations of the calculus of constructions (CC) with two kinds Prop and Type such that Prop:Type and impredicative on Prop, it is easy to show the following result:
every closed term ...
0
votes
0answers
93 views
Constraint-Based Type Inference with Algebraic Data [closed]
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 ...
4
votes
1answer
513 views
How does inheritance differ from subtyping?
In programming language perspective, what is mean by subtyping? I heard that "Inheritance is not Subtyping". Then what are the differences between inheritance and subtyping?
6
votes
3answers
551 views
Type system based on naive set theory
As I understand, in computer science data types are not based on set theory because of things like Russell's paradox, but as in real world programming languages we can't express such complex data ...
15
votes
2answers
481 views
Type classes vs object interfaces?
I don't think I understand type classes. I'd read somewhere that thinking of them as "interfaces" (from OO) that a type implements is wrong and misleading. The problem is, I'm having a problem seeing ...
7
votes
2answers
204 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 ...
4
votes
2answers
330 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 ...
