Type structure is a syntactic discipline for enforcing levels of abstraction.
2
votes
0answers
131 views
What kinds of programming pitfalls modern languages are able to express? [migrated]
I often see claims that modern functional strictly-typed languages are 'safer' than others. These statement mostly linked with type systems and their ability to explicitly express the following ...
7
votes
1answer
162 views
What is the categorical semantics of subtyping?
Starting from Curry-Howard-Lambek, there has been a nice trinity of type theories, logics, and categories. I'm curious what categorical semantics you get when you add (coercive) subtyping to a type ...
9
votes
1answer
165 views
What is the difference between arrows and exponential types in the cartesian closed category?
In a Cartesian Closed Category (CCC), there exist the so-called exponential objects, written $B^A$. When a CCC is considered as a model of the simply-typed $\lambda$-calculus, an exponential object ...
3
votes
1answer
96 views
Decidability in Extensional Type Theory
What are the ways in which one can add a decidable equivalence relation in a type system with undecidable type checking/extensional equality?
18
votes
2answers
3k views
What is the logarithm or root operation in type-space?
I was recently reading The Two Dualities of Computation: Negative and Fractional Types. The paper expands on sum-types and product-types, giving semantics to the types ...
6
votes
1answer
164 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 ...
12
votes
3answers
330 views
funsplit and polarity of Pi-types
In a recent thread on the Agda mailing list, the
question of $\eta$ laws popped up, in which Peter Hancock made thought-provoking remark.
My understanding is that $\eta$ laws come with negative
...
0
votes
0answers
60 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
95 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 ...
5
votes
2answers
416 views
Certified compiler and optimizations in Coq/Agda
I am interested in verified compilers formalized in Martin-Löf type theory, i.e. Coq/Agda. At the moment I’ve written a small toy example. Therewith I can prove that my optimizations are correct. For ...
4
votes
0answers
151 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 ...
10
votes
3answers
314 views
How is duality of types defined?
In Wadler's Recursive Types for Free! [1], he demonstrated two types, $\forall X . (F(X) \rightarrow X) \rightarrow X$ and $\exists X . (X \rightarrow F(X)) \times X$, and claimed they are dual. In ...
6
votes
3answers
197 views
“Guarded” negative occurrences in definition of inductive types, always bad?
I know how some negative occurrences can definitively be bad:
...
9
votes
1answer
113 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 ...
6
votes
1answer
260 views
Will Martin-Löf Type Theory lead to a greater ability to write provably correct code?
This post refers to the Curry-Howard isomorphism and the Martin-Löf Type Theory.
The post makes the claim of a future 'unification' between the the describing language of math, and the operation ...
1
vote
1answer
97 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 ...
8
votes
2answers
132 views
Closure ordinals for inductive types with function spaces
Functors built from finite products and sums have closure ordinal $\omega$, detailed nicely in
this manuscript by Francois Metayer. i.e. we can reach the inductive type $nat := \mu X. 1 + X$ by ...
11
votes
1answer
450 views
Explaining Applicative functor in categorical terms - monoidal functors
I'd like to understand Applicative in terms of category theory.
The documentation for Applicative says that it's a strong lax ...
7
votes
1answer
218 views
Reading list on rewriting systems?
I am new to studying rewriting systems as a first year PhD student. I would like to propose a special topics course on rewriting theory, and I want to make sure I don't leave any of the original ...
5
votes
2answers
440 views
Do Higher-Order Functions provide more power to Functional Programming?
My original question was: Is Kappa calculus less powerful than Lambda calculus?
Does the lack of Higher-Order functions on a programming language excludes some programs that could only be written in ...
3
votes
0answers
102 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 ...
4
votes
1answer
535 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?
10
votes
2answers
513 views
What's the difference between ADTs, GADTs, and inductive types?
Might anyone be able to explain the difference between:
Algebraic Datatypes (which I am fairly familiar with)
Generalized Algebraic Datatypes (what makes them generalized?)
Inductive Types (e.g. ...
3
votes
2answers
255 views
Confusing (to me) statement from “Type Classes in Haskell”
I'm reading up on type classes, and started looking at the paper Type Classes in Haskell.
In Section 2.2 - Superclasses, the authors use the following example:
...
8
votes
0answers
365 views
Can boolean algebra be expressed in simply typed lambda caclulus?
Boolean algebra can be expressed in untyped lambda calculus in (for example) this way.
...
17
votes
6answers
1k views
What is the difference between propositions and judgments?
I get confused by the subtle difference between propositions and judgments when exposed to intuitionistic type theory. Can any one explain to me what is the point to distinguish them and what ...
6
votes
3answers
554 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
491 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 ...
5
votes
6answers
1k views
Functions that typed lambda calculus cannot compute
I just want to know some examples of the functions that can be computed by the untyped lambda calculus but not by typed lambda calculi.
As I am a beginner, some reiteration of background information ...
7
votes
1answer
142 views
How to define eta-equivalence for F-omega types?
There are (at least) two styles for defining a (declarative) equivalence judgement for a typed lambda calculus:
via a plain relation $t_1 = t_2$,
via an indexed relation $\Gamma \vdash t_1 = t_2 : ...
9
votes
3answers
310 views
Modeling objects (OOP) in dependent type theory
I am interested in modeling objects, from object oriented programming, in dependent type theory. As a possible application, I would like to have a model where I can describe different features of ...
6
votes
3answers
416 views
Boolean as subtype of integer
In languages oriented towards systems programming, digital logic and hardware design, it's common to treat boolean as a subtype of integer. In languages oriented towards mathematics and type theory, ...
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 ...
8
votes
2answers
821 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 ...
12
votes
1answer
221 views
Barendregt's proof of subject reduction for $\lambda2$
I found a problem in Barendregt's proof of subject reduction (Thm 4.2.5 of Lambda calculi with types).
The last step of the proof (page 60), says:
"and hence by Lemma 4.1.19(1), ...
12
votes
3answers
442 views
Can we prove weak normalization for System F by induction on a transfinite ordinal
Weak normalization for the simple typed lambda calculus can be proved (Turing) by induction on $\omega^2$. An extended lambda calculus with recursors on natural numbers (Gentzen) has a weak ...
16
votes
2answers
557 views
Is there an expressiveness hierarchy for type systems?
Inspired by the extensive hierarchies present in complexity theory, I wondered if such hierarchies were also present for type systems. However, the two examples I've found so far are both more like ...
13
votes
2answers
320 views
Proof theory of biproducts?
A category has biproducts when the same objects are both the products and coproducts. Has anyone investigated the proof theory of categories with biproducts?
Perhaps the best-known example is the ...
7
votes
0answers
331 views
What's the relation and difference between Calculus of Inductive Constructions and Intuitionistic Type Theory?
As stated in the title, I wonder any relation and difference between CIC and ITT. Could someone explain or point to me some literature that compares these two systems? Thanks.
6
votes
1answer
241 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}$ ...
12
votes
2answers
324 views
What are the equational laws for zero types?
Disclaimer: while I care about type theory, I don't consider myself an expert on type theory.
In the simply typed lambda calculus, the zero type has no constructors and a unique eliminator:
...
15
votes
1answer
480 views
Seeking Scott's original LCF paper
Is the following manuscript publically available?
Dana Scott, 1969, A theory of computable functions of higher type. Unpublished seminar notes, 7 pages, University of Oxford.
There is a ...
6
votes
1answer
257 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
240 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' ...
8
votes
2answers
208 views
Does the order of declarations in an inductive type matter?
I was wondering if the order of declarations of an inductive type can matter.
For example in Coq you can define Nat either by:
...
14
votes
2answers
476 views
Do dependent types give you everything subtyping does?
Types and Programming Languages focuses quite a bit on subtyping, but as far as I can tell, subtyping doesn't seem especially fundamental. Does subtyping give you anything more than dependent types ...
25
votes
1answer
731 views
Inductive types for large countable ordinal notations.
I'm looking to build notations for large countable ordinals in a "natural way". By "natural way" I mean that given an inductive data type X, that equality should be the usual recursive equality (the ...
17
votes
5answers
1k views
What is the most intuitive dependent type theory I could learn?
I am interested in getting a really solid grasp on dependent typing. I've read most of TaPL and read (if not fully absorbed) 'Dependent Types' in ATTaPL. I've also read and skimmed a bunch of articles ...
10
votes
3answers
481 views
What is the role of predicativity in inductive definitions in type theory?
We often want to define an object $A \in U$ according to some inference rules. Those rules denote a generating function $F$ which, when it is monotonic, yields a least fixed point $\mu F$. We take $A ...
11
votes
2answers
260 views
References to programming languages based on conditional logics
Conditional logics are logics which augment traditional logical implication with modal operators corresponding to other notions of condition (for example, the causal conditional $A\; ...
