formal systems to specify properties of objects

learn more… | top users | synonyms

4
votes
0answers
26 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
46 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
48 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
40 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
37 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
54 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
54 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 ...
4
votes
0answers
45 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
51 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
103 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
40 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
54 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
31 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
37 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, ...
0
votes
2answers
57 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
24 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
206 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
122 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 / ...
3
votes
2answers
96 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
42 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
113 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
173 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
54 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
68 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
64 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 ...
5
votes
2answers
419 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
123 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
76 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
103 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
49 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
85 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
78 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
35 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
79 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
36 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
82 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
219 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
133 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
129 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 ...
8
votes
3answers
446 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: ...
4
votes
2answers
106 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
52 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 ...
5
votes
3answers
520 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
136 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 ...
4
votes
2answers
188 views

Universes in dependent type theory

I am reading about dependent types theory in the Homotopy Type Theory online book. In section 1.3 of the Type Theory chapter, it introduces the notion of hierarchy of Universes: $\mathcal{U}_0 : ...
3
votes
2answers
130 views

To what does typing correspond in a Turing Machine?

I hope my question makes sense: Starting with the premise that the untyped $\lambda $ calculus is equivalent in power to a Turing machine, to what in a Turing machine does adding types to the $\lambda ...
6
votes
1answer
191 views

Example of a false proposition when assuming Type : Type

In Type Theory if one allows Type to be a member of itself, it makes the theory inconsistent. I understand it by analogy to Russel's paradox in Set Theory, but would prefer to see it done in Type ...
3
votes
1answer
181 views

What kinds of programming pitfalls modern languages are able to express?

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 ...
10
votes
1answer
483 views

What makes type inference for dependent types undecidable?

I have seen it mentioned that dependent type systems are not inferable, but are checkable. I was wondering if there is a simple explanation of why that is so, and whether or not there is there a limit ...