formal systems to specify properties of objects

learn more… | top users | synonyms

2
votes
1answer
72 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 ...
2
votes
0answers
33 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
32 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
26 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
34 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
43 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
21 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
187 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
104 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
52 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 ...
1
vote
1answer
35 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
94 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
140 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
52 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
63 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
62 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 ...
4
votes
1answer
148 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 ...
4
votes
1answer
92 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
62 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
71 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
45 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
81 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
63 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
30 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
53 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
32 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
78 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
209 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
109 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
109 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
48 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
298 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
98 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
51 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
467 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
123 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
170 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
122 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
175 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
178 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
340 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 ...
0
votes
1answer
83 views

Is constant a variable or subtype?

I think of type as a range of values that the variable can take whereas the rest is known constant or does not matter. Variables (instances or objects), which share common properties, are considered ...
2
votes
0answers
103 views

Encoding row types

I'm working on a type system with extensible records, similar to ones explained in "A Polymorphic Type System for Extensible Records and Variants - Benedict R. Gaster and Mark P. Jones" and ...
4
votes
1answer
180 views

What is the difference between the semantic and syntactic views of function types?

Edit: My original question referred to nonconstructive and constructive definitions of function types. I changed the terminology in the question and the title to semantic and syntactic, which the ...
10
votes
2answers
476 views

How are programming languages and foundations of mathematics related?

Basically I am aware of three foundations for math Set theory Type theory Category theory So in what ways are programming languages and foundations of mathematics related? EDIT The original ...
5
votes
3answers
249 views

How can SML infer types like this?

Wikipedia says: fun factorial n = if n = 0 then 1 else n * factorial (n-1) A Standard ML compiler is required to infer the static type int -> int of ...
8
votes
1answer
323 views

Concise example of exponential cost of ML type inference

It was brought to my attention that the cost of type inference in a functional language like OCaml can be very high. The claim is that there is a sequence of expressions such that for each expression ...
3
votes
3answers
226 views

Why classes implicitly derive from only the Object Class?

I do not have any argument opposing why we need only a single universal class. However why not we have two universal classes, say an Object and an AntiObject Class. In nature and in science we find ...
8
votes
1answer
145 views

Inferring refinement types

At work I’ve been tasked with inferring some type information about a dynamic language. I rewrite sequences of statements into nested let expressions, like so: ...
14
votes
1answer
504 views

Does there exist a Turing complete typed lambda calculus?

Do there exist any Turing complete typed lambda calculi? If so, what are a few examples?