formal systems to specify properties of objects

learn more… | top users | synonyms

5
votes
2answers
51 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
34 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
42 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
204 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
50 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
38 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
52 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
60 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 ...
3
votes
1answer
48 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
45 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
58 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
69 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 ...
6
votes
2answers
70 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
57 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
111 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 ...
3
votes
0answers
41 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
59 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
34 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
49 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
65 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
25 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
219 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
133 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 / ...
4
votes
2answers
166 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
46 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 ...
4
votes
2answers
115 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
194 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
56 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
82 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
70 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 ...
6
votes
2answers
615 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 ...
7
votes
1answer
137 views

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

I'm reading about this 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 arguments will determine ...
2
votes
1answer
81 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
129 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
51 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
87 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
93 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
36 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
88 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
37 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 ...
-1
votes
1answer
84 views

Type for difference of two absolute values

I always see that people in the fields consider confusing vectors with positions as a severe error in one and n dimensions. Recently I have also encoutered a timedelta type in Python. By increadably ...
2
votes
3answers
222 views

What would dynamically-typed languages actually do if type enforcement was removed?

I program in Python, which is a well-known dynamically typed language. I understand dynamic typing to mean mainly that "operations" (in a loose sense) in the language are either allowed or denied ...
2
votes
1answer
163 views

Java, strong typing, covariance and contra-variance

While studying for a test in my OOP course, I came upon this question which had an answer I didn't really understand. The question is as follows (translated): The programming language "Sava" is ...
0
votes
2answers
145 views

does godel's incompleteness theorem shed any light on dynamic vs typed languages? [closed]

I'm clojure user myself. I'm trying really hard to learn haskell and to better understand the type system. However, I feel that trying to 'type' everything is quite restrictive when the problem or the ...
3
votes
1answer
53 views

Type inference of pair (product) types

I am looking into Hindler-Milney type system and I am trying to add support for the pair type. In Pierces book, he introduces special language constructs for creation of pairs and getting their ...
9
votes
3answers
586 views

Intro to Martin-Löf type theory

What would be the best introduction to Per Martin-Löfs ideas about type theory? I've looked at some lectures from the Oregon PL summer school, but I'm still sort of puzzled by the following question: ...
5
votes
2answers
111 views

Example of existence proof in dependent typing?

I understand that $\Pi$ types are generalizations of functions and can be interpreted similar to $\forall$ in logic. I also know that $\Sigma$ types are generalizations of tuples and can be ...
0
votes
1answer
54 views

Looking for cheat sheet to J.C. Reynolds symbols

Most specifically, his use of small epsilon introduced at the end of section 1 of "Types, Abstraction and Parametric Polymorphism" is throwing me, but in general I would like references to symbols in ...
6
votes
3answers
550 views

Type theory and type systems

I recently realized that there is some sort of relation between Russellian type theory and type systems, as found e.g. in Haskell. Actually, some of the notation for types in Haskell seems to have ...
3
votes
1answer
140 views

lambda calculus as a type theory

From the Introduction section of Homotopy Type Theory book: Type theory was originally invented by Bertrand Russell ... It was later developed as a rigorous formal system in its own right(under ...