formal systems to specify properties of objects

learn more… | top users | synonyms

3
votes
0answers
42 views

What are the strongest known type systems for which inference is decidable?

It's well known that Hindley-Milner type inference (the simply-typed $\lambda$-calculus with polymorphism) has decidable type inference: you can reconstruct principle types for any programs without ...
3
votes
1answer
38 views

Top-down typing strategy - is there a name for this?

In most statically typed languages, each expression has an intrinsic type. E.g. in Java, 3 is an int, 3.0 is a double, ...
3
votes
2answers
50 views

Isn't Domain of a variable nothing but a constraint?

In Constraint programming we have Variables and their Domains and then all the constraints, but if you at the concept of a domain of a variable it is nothing but another type of constraint, you are ...
3
votes
0answers
24 views

Is the strictly positive condition in Coq and Agda an aproximation?

Languages like Coq and Agda enforce that their inductive types occur "strictly positively" in their definitions. That is, the type should not occur to the left of an arrow of an argument of a ...
1
vote
1answer
25 views

Rearranging function in 'Theorems for free'

I'm reading Wadler's 'Theorems for free'. In section 3.5 he states that $m_{AA}(I_A)$ is a rearranging (i. e. injective) function. $I_A$ is the identity function on the type A. $$m : \forall X.\forall ...
4
votes
1answer
48 views

Meaning of “positive position” and “negative position” in type theory?

What does "in positive position" and "in negative position" mean in the context of type theory? The only thing I understood from Bob Harper's blog post on the topic is that there is a connection ...
3
votes
1answer
36 views

How to understand equivalence of indexes of a family of types that are not definitionally equal

So I've been reading things about HoTT and trying to get solid on the foundations before getting too much further into the book. I am confused by a certain point; maybe I just haven't read far enough ...
1
vote
2answers
46 views

Why have a numeric type hierarchy?

The more I think about it, the stranger the concept of having a number type, which is a super-type of integers, rationals and reals seems to be. One thing that ...
0
votes
1answer
42 views

Can polymorphism be simulated by lazy type operators?

In the definition of lambda cubes, type polymorphism is distinguished from type operators/constructors. I have the nagging feeling that type polymorphism can be constructed through type operators ...
3
votes
1answer
59 views

type theory notation troubles

I'm working through "Types and Programming Languages" by Benjamin Pierce and I don't quite understand the notation. Particularly on Page 106, (chapter 9 Simply Typed Lambda-Calculus) there is a lemma ...
4
votes
0answers
42 views

Main differences between intuitionistic type theory and calculus of constructions (CoC)

Quoting Wikipedia "Many systems of type theory, such as the simply-typed lambda calculus, intuitionistic type theory, and the calculus of constructions, are also programming languages." I'm a Coq user ...
8
votes
0answers
121 views

Why do we have to forbid non-conforming lower and upper type bounds?

(it's a repost of my unanswered question from scala-user@googlegroups.com about Scala) In the Scala Language Specification, §4.4 Type Parameters, there is a requirement: The most general form of ...
4
votes
2answers
43 views

Algorithmic type checking for Calculus of Inductive Constructions

So from reading "Advanced Topics in Types and Programming Languages" (ATTPL) I know of the calculus of constructions (CoC). It also presents the "algorithmic" type checking rules. Reading Coq's ...
5
votes
2answers
93 views

Application of set theory subjects as ordinals, forcing, generic filters in software engineering

I am going to teach a course in set theory for software engineering students. I am going to talk in this course about: ordinal numbers, partial orders, well ordering, generic filters and maybe some ...
1
vote
0answers
9 views

Importance of indexes in Type(i) in calculus of inductive constructions [duplicate]

So I am reading about the calculus of inductive constructions. And I see here and here that there hidden indexes that the user does not know about in the $Type$ sort. It says that they are ...
1
vote
2answers
50 views

Given the “programs as proofs” isomorphism, how do we know that the program isn't lying?

I've been studying constructive type theory (CTT) and one of the things that I'm not clear on is the proof part: Proving the correctness of a program in a form of a proof that's nothing but the ...
6
votes
2answers
119 views

What do we gain by having “dependent types”?

I thought I understood dependent typing (DT) properly, but the answer to this question: Why was there a need for Martin-Löf to create intuitionistic type theory? has had me thinking otherwise. ...
3
votes
0answers
90 views

Row polymorphism, union and intersection types

It seems that row polymorphism with union types can be used in dynamic languages to approximate overloading, e.g. given the following python function: ...
1
vote
0answers
89 views

Is there a formalization of automatic-splicing data structures?

I'm wondering if there is some formalization, type theoretical analysis, or similar for data structures that automatically "splice" in an associative way. Barring a perfect citation, I'd be interested ...
2
votes
0answers
53 views

Test cases for subtyping with dependent types

I implemented a simple type system inside Agda and I'm trying to understand, how expressive it is. The system consists from a predicative hierarchy of universes in the style of Russell, natural ...
3
votes
2answers
47 views

Definition of a size of type

In B. Pierce's book "Types and Programming Languages", he talks about the size of types (see pictures below). I searched the book for a definition but could not find one. I only found a definition ...
2
votes
0answers
31 views

Understanding a paper on polynomial recursion in all finite types

So I wasn't sure weather or not this counted as "research level" or not but I figured it wasn't so I decided to post it here. There is a paper by S. Bellantoni et al. called "Higher Type Recursion, ...
0
votes
1answer
50 views

Pierce's Types and Programming Languages : circular definition of terms?

In Pierce's book, on page 26-27 it is given a definition of terms for a simple language using inference rules. In the picture below it is marked by red highlighting the problematic part. What is ...
10
votes
1answer
228 views

Why aren't we researching more towards compile time guarantees?

I love all that is compile time and I love the idea that once you compile a program a lot of guarantees are made about it's execution. Generally speaking a static type system (Haskell, C++, ...) seems ...
2
votes
2answers
72 views

Understanding constraint formula concept in Java

JLS defined a concept called "constraint formula". There is a formal definition: Constraint formulas are assertions of compatibility or subtyping that may involve inference variables. The ...
6
votes
2answers
179 views

Does the Y combinator contradict the Curry-Howard correspondence?

The Y combinator has the type $(a \rightarrow a) \rightarrow a$. By the Curry-Howard Correspondence, because the type $(a \rightarrow a) \rightarrow a$ is inhabited, it must correspond to a true ...
3
votes
1answer
50 views

How can finite sets be represented as a type?

Manually self-migrated from stack overflow. A set of objects of a type T is often represented using its indicator function (set T = ...
5
votes
2answers
107 views

Which fixpoint is Haskell list type?

Let's say that lists are defined as List a = Nil | Cons a (List a) Then, in Haskell is List x the greatest or least fixpoint? ...
1
vote
1answer
51 views

Weakening and Contraction

Wikipedia says that weakening is a structural rule where the hypotheses or conclusion of a sequent may be extended with additional members and that contraction is a rule where two equal (or unifiable) ...
4
votes
1answer
68 views

Can coq express its own metatheory?

I'm learning about language metatheory and type systems, and am using coq to formalize my study. One of the things I'd like to do is examine type systems that include dependent types, which I ...
5
votes
2answers
233 views

What is the connection between data structures and data types?

I have read some books and wikipedia, which seem to give not completely consistent definitions and notations. I try to understand the concepts, regardless of what they are called. Here are what I have ...
0
votes
1answer
60 views

Does modern type theory include specifications and implementations?

Good programming practice distinguishes between specification (at the API level) and implementation. I would have thought that this same distinction would be found in type theory. Perhaps I just don't ...
5
votes
0answers
49 views

Bounded existential polymorphism

In Pierce's "Types and Programing Languages" he, at the very end, presents the most powerful system in the book: $F^{\omega}_{<:}$. He, however, does not explain how bounded existential ...
5
votes
1answer
71 views

What is $Prop$ in the calculus of constructions?

I'm looking at the Calculus of Constructions and its place in the Lambda Cube. If I understand correctly, each axis of the cube can be thought of as adding another operation involving types to the ...
1
vote
1answer
94 views

Video lectures on type systems

For my job, I need to pick up a working understanding of the implementation of type systems (in particular, how to write typing rules based on a design document). I've been given a copy of Types and ...
5
votes
1answer
88 views

Can I have a “dependent coproduct type”?

I'm reading through the HoTT book and I have a (probably very naive) question about the stuff in the chapter one. The chapter introduces the function type $$ f:A\to B $$ and then generalizes it by ...
2
votes
0answers
52 views

Are there models of type theory that allow the real numbers to be a type?

Do there exist models of type theory that allow types to contain an uncountable number of inhabitants? Traditionally type theory seems to be swirled in with computable programs as constructive proofs ...
5
votes
1answer
66 views

Unrolling multi-variable mu (μ) expressions in type theory

Unrolling an iso-recursive μ-type expression such as, say, one isomorphic to natural numbers: μα.1+α using ...
4
votes
1answer
142 views

Why are dependently typed languages such as Agda used for proofs, if supercompilers for simpler typed languages can do the same?

Proof assistants such as Agda can be used to assert properties about programs, such as "the double of a number is even". Interestingly, supercompilers can be used for the same purpose, creating ...
6
votes
2answers
81 views

Type of a return satement

I'm creating a experimental toy language for my own education purposes (an impure typed Lisp based on Clojure - https://github.com/mikera/kiss) I think I understand the concept of each expression in ...
5
votes
1answer
86 views

Type inference + overloading

I'm looking for a type inference algorithm for a language I'm developing, but I couldn't find one that suits my needs because they usually are either: à la Haskell, with polymorphism but no ad-hoc ...
5
votes
1answer
133 views

What does Tarski's Fixed-Point theorem give us that that Y-Combinator does't

I'm taking a graduate course on the theory of functional programming, based on Paul Taylor's "Practical Foundations of Mathematics." I understand the statement of Tarski's theorem about how for any ...
4
votes
0answers
57 views

Does there exist a type system for a non-let-polymorphic lambda calculus?

I'm wondering if there is a way to extend Hinley-Milner's type system to allow polymorphic types without the need of a let construct, by adding an intersection type (as Dan pointed out) that ...
0
votes
2answers
90 views

Role of Term Constants in Simply Typed Lambda Calculus

In the Wikipedia article on Simply Typed Lambda Calculus (among other places), there is a notion of a "term constant". This is particularly notable in the production grammar given: In this ...
0
votes
1answer
37 views

Verify the type of a lambda expression

I need to verify the type for the lambda expression: $\lambda f.\lambda x.f (f x)$ My method gives me: $(a\rightarrow c)\rightarrow b\rightarrow c$ Im trying to define it in Haskell (on Hugs) like ...
3
votes
1answer
92 views

What is an reflective tower?

I've just read in a discussion about dynamic typing Reflective towers is an open problem for statically typed languages. What are reflective towers? I think it might be related to reflection, ...
1
vote
2answers
99 views

Rule induction principles in Harper's PFPL

I have a few small questions about section 2.4 ("Rule induction") in Practical Foundations for Programming Languages (p. 19). (1) In the rule induction principles for ...
1
vote
0answers
32 views

Type systems understanding problems

I'm not sure if this is the correct place to ask this kind of a question, but here goes: I'm doing my own reading of the Principles of Program Analysis book, and i'm having trouble understanding some ...
11
votes
4answers
255 views

Has Anyone Actually Created a System that Writes Computer Programs from specification?

Has anyone ever actually written a system (software or detailed explanation on paper with simple examples) that generates computer programs? I input $Prime(x) \wedge x<10$ and it creates a program ...
1
vote
1answer
153 views

When do type systems start needing a logic engine?

I've noticed that some languages include a logic engine as part of their type system (e.g. Shen, Typed Clojure). Other languages have a much more direct type checking algorithm (e.g. Haskell / ...