formal systems to specify properties of objects

learn more… | top users | synonyms

3
votes
0answers
52 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
85 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
47 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
45 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
30 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
35 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 ...
7
votes
0answers
185 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
68 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
110 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
44 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
80 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
42 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
52 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
230 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
56 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
47 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
64 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
72 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 ...
4
votes
1answer
68 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
49 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
65 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 ...
3
votes
1answer
113 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
75 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
72 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
120 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
51 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
73 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
35 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
71 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
84 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
27 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
236 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
144 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 / ...
7
votes
2answers
318 views

Dependent types vs refinement types

Could somebody explain the difference between dependent types and refinement types? As I understand it, a refinement type contains all values of a type fulfilling a predicate. Is there a feature of ...
2
votes
1answer
52 views

Is this a well founded inductive type? Can I express this in Coq?

the standard List type in Coq can be expressed as: Inductive List (A:Set) : Set := nil : List A | cons : A -> List A -> List A. as I understand, W-type ...
5
votes
2answers
133 views

What are the difference between and consequences of using type parameters and type indexes?

In type theories, like Coq's, we can define a type with parameters, like this: ...
6
votes
2answers
282 views

Define a list using only the Hindley-Milner type system

I'm working on a small lambda calculus compiler that has a working Hindley-Milner type inference system and now also supports recursive let's (not in the linked code), which I understand should be ...
2
votes
4answers
58 views

Are references of any use without updating?

Almost all type-theoretical treatments of references that I've studied introduce references as accompanied with at least three operations (sometimes including the fourth): Construction (allocation): ...
0
votes
2answers
86 views

How is a type system related to a progam?

In another question about Lambda Calculus, Andrej Bauer made the comment: Lambda calculi of various forms are formal systems. They consist of abstract syntax (for terms and for types, if ...
4
votes
1answer
97 views

Can parameters be contra- or covariant in Python?

I've just now studied about covariance and contravariance in static languages (more specifically C#). This concept is rather clear to me, however I'm in doubt on how this applies to dynamic languages ...
13
votes
2answers
1k views

What can Idris not do by giving up Turing completeness?

I know that Idris has dependent types but isn't turing complete. What can it not do by giving up Turing completeness, and is this related to having dependent types? I guess this is quite a specific ...
8
votes
1answer
186 views

Why will the Hindley-Milner algorithm never yield a type like t1 -> t2?

I'm reading about the Hindley-Milner typing algorithm while writing an implementation, and see that, as long as every variable is bound, you'll always get either atomic types or types where the ...
2
votes
1answer
104 views

Would adding recursive named functions to Simply typed lambda calculus make it Turing complete?

Say I have Simply typed lambda calculus, and add an assignment rule: <identifier> : <type> = <abstraction> Where ...
1
vote
2answers
166 views

Is Wadler's 'Theorems for Free' as general as Design By Contract for establishing correctness?

Philip Wadler has written a brilliant paper called 'Theorems for Free'. The big idea is that you can use types to reason about your program, and even prove simple theorems about your program. We see ...
4
votes
1answer
56 views

In type systems, is there a name for SQL's way of cutting and combining record types into new types?

I'd like to have this feature in my application programming language (which these days, is Scala), but when I went to learn more about it on the internets, I realized I don't know the name of it. I'm ...
3
votes
1answer
90 views

What do functions look like, if I stated out with the categoical model of my type theory?

I see how objects in a category stand for types, but where do I find the terms and more specifically the rules which tell me which of them are allowed? When I e.g. consider a Cartesian closed category ...
3
votes
1answer
116 views

Non-termination of types in Martin-Löf's Type:Type?

In the pre-history of dependent type theory, Per Martin Löf introduced a calculus that is in some sense the simplest dependent type theory and the most general form of impredicative polymorphism. It ...
1
vote
1answer
45 views

Does types being terms imply your dependend theory is considered polymorphic?

In the introduction of the book by B.Jacobs, "Categorical Logic and Type Theory" (it's online here), he classifies type systems into three general flavours: Simply typed ones, depended typed (term ...
1
vote
2answers
98 views

If dynamically typed languages are truly statically typed, unityped languages, what is the (finite) type expression of the one type?

Some claim that dynamically typed languages are in reality statically typed, unityped languages. This would imply to me that this one type should be expressible as a static, finite type expression, so ...
0
votes
1answer
40 views

Are Algebraic types just the combination of case classes and pattern matching?

On this page describing the precursor to the Scala language - the pizza language - they refer to it having both case classes and pattern matching - and then imply that these taken together provide ...