formal systems to specify properties of objects

learn more… | top users | synonyms

2
votes
2answers
92 views

Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program?

Chapter 7 of The Haskell Road to Logic Math and Programming discusses induction and recursion. Haskell is strongly typed and we can define the natural numbers ...
5
votes
3answers
1k views

Which research languages have a stronger typesystem than Haskell and why?

Here I read that: Haskell definitely does not have the most advanced type system (not even close if you count research languages) but out of all languages that are actually used in production ...
4
votes
1answer
55 views

How to prove $0\neq1$ using the J rule?

Suppose I have a simple dependent type theory with bottom, unit, sums, dependent pairs, dependent functions, natural numbers and homogeneous identity with J-elimination. Is there a way to prove $(0 = ...
1
vote
1answer
31 views

What is the rationale behind implicitly widening integer types in numeric operations?

Languages such as Java and C specify implicit widening of integer types for numeric operators, especially arithmetic operators, to a minimum of 32 bits. What is the rationale behind doing this? My ...
6
votes
0answers
17 views

Is there any type system which can assign a type to any halting lambda calculus term? [duplicate]

Some lambda terms, such as the church number 3: (f x -> (f (f (f x)))), are easily typeable on the simply typed lambda calculus. Others, such as ...
4
votes
0answers
64 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
53 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
3answers
70 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
30 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
172 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
39 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
51 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
45 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
72 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
50 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
128 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
46 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
134 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
51 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
126 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
115 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
90 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
55 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
50 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
36 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
55 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
249 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
82 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
196 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
55 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
120 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
53 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
71 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
245 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
61 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
50 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
72 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
97 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 ...
6
votes
1answer
97 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
72 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
161 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
83 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
94 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
137 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
61 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
91 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
38 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 ...