formal systems to specify properties of objects

learn more… | top users | synonyms

3
votes
1answer
39 views

System f-sub, how to do type checking?

I was reading that system f-sub (polymorphic lambda calculus with sub-typing) and I was quite confused with its one checking rule called "T-TAPP". This rule as following (ctx denotes the typing ...
6
votes
1answer
55 views

Is there any difference between extensible records and dependent maps

In a typed setting, records can be thought of as a map from field to type. If there is a well-typed record merge operation (which allows overlapping fields), is there any real difference between the ...
7
votes
2answers
169 views

Type-system combining type-states and typed effects?

Has anyone succeeded in implementing or designing a type-system that combines both type-state (linear types) and effect types (e.g. Koka)?
-1
votes
0answers
34 views

Relation between Application and Substitution principle

Using type application rule. I think it states that : if you have a proof of T11 -> T12 and a proof of T11 you can get a proof of T12. It seems that we have to do substitution here. $$\dfrac{ \Gamma ...
7
votes
0answers
100 views

Are type constructors always injectives even in presence of quantified type variables (subtyping)?

Are type constructors, in a language that feature subtyping and quantification of type variables, like scala or Java, always injective? That is, is an equivalent of haskell ...
4
votes
2answers
76 views

Is there a relationship between “sound and complete” in logic and “type safety” in PLs?

I've been wondering if there's a connection between "good logics" and "good programming languages". It seems that logics are shown to be "locally sound and complete" whereas programming languages are ...
1
vote
2answers
59 views

The range of significance in Type Theory

What exactly does "Types as ranges of significance of propositional functions. In modern 
terminology, types are domains of predicates" mean? Update: I found in this paper (Pag 14 or 234) by Russell, ...
8
votes
1answer
91 views

Origin of the concept of types

About the state of art that I'm running ahead of Type Theory I have the these questions all related about history of Types. Where did the idea of Type come from? (It seems that all start when ...
0
votes
1answer
76 views

Indexing a dependent type on a value?

If i'm recalling from Robert Harper's lectures Homotopy type theory A dependent type is a family of type index by a type. If we allow index to be just a value can we gain something instead of allowing ...
1
vote
0answers
33 views

DML , ML with restricted dependent types

Refering to this paper Dependent ML: An Approach to Practical Programming with Dependent Types Have defined datatype 'alist ( int ) Its not clear why they have used int as a parameter rather than a ...
1
vote
2answers
72 views

Strict positivity

From This reference : Strict positivity The strict positivity condition rules out declarations such as ...
3
votes
1answer
170 views

Family of types in type theory

Can anyone simplify the meaning of families of types index by a type. It looks i get it but quite not understood it. What do you mean by a "family" ? I understand index by a value (n length sequence)...
3
votes
2answers
61 views

Meaning of , and ; in relation to defining context

I have seen use of , and somewhere use of ; when defining context : $$\dfrac{\phi \ , \ \Gamma \ \vdash } {} $$ somewhere else i have seen : $$\dfrac{\phi \ ; \ \Gamma \ \vdash ...
3
votes
3answers
115 views

How to use Type application Rule to get a desired type

In type application Rule : $$\dfrac{ \Gamma \vdash t_1 : T_{11} \to T_{12} \qquad \Gamma \vdash t_2 : T_{11}} { \Gamma \vdash t_1 \ t_2 : T_{12} } \textsf{ (T-App)}$$ if we ...
0
votes
0answers
59 views

Type inference and Type checking

I understand that adding the annotations (dependent typing) may cause the type checking of the programming language to become undecidable. What about type inference ? Whether type checking and type ...
7
votes
1answer
67 views

Why is `map insertionsort` not to equal to`map mergesort`?

In the type theory podcast ep. 3, Dan Licata claims that the fact that for every input, insertionsort and mergesort give the same result does not imply that the result would be equal when used as ...
2
votes
1answer
89 views

Variable rule in dependent type theory

This is the = Type variable rule that I'm seeing through out the my course and unable to grasp it completely. $$\dfrac{\phi \vdash \Gamma[\mathrm{ctx}] \qquad \Gamma(x) = \tau} {\phi; \Gamma ...
5
votes
1answer
71 views

How precise is the statement “STLC is the internal language of CCCs”?

I'm studying some basic category theory in the context of type theory and came across the statement "simply typed lambda calculus is the internal language of cartesian closed categories". However ...
11
votes
2answers
130 views

“Minimal” intuitionistic type theory?

I'm surprised that people keep adding new types in type theories but no one seems to mention a minimal theory (or I can't find it). I thought mathaticians love minimal stuff, don't they? If I ...
4
votes
1answer
80 views

Proving preservation under substitution System F Omega

I am going over the proofs for the simply typed lambda calculus in the book "Types and Programming languages" by Benjamin Pierce. I am trying to find inspiration for the similar proofs for System F ...
5
votes
1answer
87 views

Difference between “sort” and “universe”

A very basic question. As title, what is the difference between "sort" and "universe" in type theory? Are they interchangable? Or are there only finite number of sorts, but infinite universes?
6
votes
2answers
232 views

Generating constraints to solve dependently-typed metavariables?

In dependent-types, Miller pattern unification is used to solve a decidable fragment of higher-order unification. This allows dependently-typed languages to contain metavariables or implicit arguments....
3
votes
1answer
47 views

premiss of reduction rule (abst) of pure type systems

$$(abst) \:\frac{\Gamma, x: t_1 \vdash t_2: t_3 \quad \Gamma \vdash (x: t_1) \to t_3: s}{\Gamma \vdash (x: t_1. t_2): (x: t_1) \to t_3}$$ In this rule, why is $(x: t_1) \to t_3$ required to be an ...
1
vote
2answers
81 views

Program interpretation for static analysis

Are there any implementations, or even academic work, regarding an application capable of looking at code and inferring what the code actually intends to do? For example, we give it a program that ...
2
votes
0answers
19 views

Where does the term “Amechanicity” for type-error generation come from

I've been looking at these slides about improving type error messages for programming languages. One of the things they describe, starting at Slide 8, is the concept of amechanicity. Anytime the ...
3
votes
0answers
50 views

Describe data structure using equations

Good afternoon. At work I'm currently developing a system which takes user input (well structured) and then stores it in memory to do some processing. The input is basically a dataset formed by ...
4
votes
1answer
69 views

What does Harper mean by “class”?

I've been teaching myself type theory on and off over the past couple years. I've reach large sections of Pierce's Types and Programming Languages and Harper's Foundations of Programming Languages, ...
8
votes
2answers
270 views

Universal/existential quantification?

I'm struggling to understand the purpose of universal and existential quantification of types. I'm playing around with writing a toy language based on the calculus of constructions. I've been reading ...
4
votes
1answer
53 views

Typing dependent pattern matching

I'm curious on how to type a dependent pattern matching in a functional language. What should the rule for typing ...
1
vote
1answer
66 views

What is the Haskell-style type signature called (i.e., who is it named after)?

A type signature in Haskell is written in the following format: functionName :: (arg1Type, arg2Type) -> returnType There's a (hyphenated, after a person or ...
8
votes
2answers
194 views

Proving a sorting operation in type system

I want to know how far a type system in a programming language can be beneficial. For example, I know that in a dependently typed programming language, we can create a Vector class incorporating size ...
7
votes
1answer
76 views

What is the difference between ∀ and Π in the Calculus of Constructions?

As I've learned, the Calculus of Constructions has only two binders - $\lambda$ and $\Pi$. Morte, for example, has $\forall$ as a mere alias of $\Pi$. Yet, on the paper Self Types for Dependently ...
1
vote
0answers
15 views

What is the intuition behind a λ-term being EAL-Typeable?

λ-terms can be split in two categories: EAL and non-EAL typeable terms. It is known not only that EAL-typeable terms can be reduced to normal form in polynomial time, but that the reduction can be ...
4
votes
1answer
79 views

Do Self Types make the Calculus of Inductive Constructions obsolete?

Self Types are an extension of the Calculus of Constructions [1] that allow the language to express algebraic datatypes encoded through the Scott Encoding. The Scott Encoding provides one the ability ...
2
votes
1answer
71 views

Why do we distinguish between term abstraction and type abstraction in System F?

In System F, we distinguish between types and terms. Types are defined by the following BNF: \begin{align} A, B ::=&~\alpha && \text{(type variable)} \\ &|~A \rightarrow B &...
4
votes
1answer
146 views

What does Godels Incompleteness theorem “true but unprovable” mean?

I have asked this on the "computer science chat" ( vzn tried to explain me ) . I even watched a couple a videos to understand the theorem but still cannot convince myself. The following is the way the ...
1
vote
0answers
23 views

What is a proof of normalization of Motte?

It is said that any term on the calculus of construction halts. I am studying it through Morte, which is a bare bone implementation of the coc available on github. Is there any simple proof of ...
23
votes
3answers
207 views

What is a brief but complete explanation of a pure/dependent type system?

If something is simple, then it should be completely explainable with a few words. This can be done for the λ-calculus: The λ-calculus is a syntactical grammar (basically, a structure) with a ...
4
votes
2answers
36 views

What terms type systems exclude?

I understand type systems like the simply typed lambda calculus, system F and the calculus of constructions include a different subset of all lambda terms. But what, precisely, are the terms each of ...
8
votes
5answers
799 views

Daily Applications of Type Theory

I want to understand type theory but I have to know first how I can apply it. Could there be more non-obvious applications of type theory aside from in type systems in programming? Could there be ...
6
votes
2answers
351 views

In the Curry-Howard isomorphism as applied to Hindley-Milner types, what proposition corresponds to a -> [a]?

(Using Haskell syntax, since the question is inspired by Haskell, but it applies to general Hindley-Milner polymorphic type systems, such as SML or Elm). If I have a type signature ...
5
votes
1answer
77 views

What is the Curry-Howard analogue for linear logics?

As defined by Wikipedia, (The Curry-Howard correspondence) is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the ...
2
votes
1answer
18 views

Can big-step semantics express evaluation order?

Can you express evaluation order using big-step semantics? For example, in a simple language consisting of only if t then t else t and ...
3
votes
2answers
158 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 ...
8
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
67 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
38 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
25 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 ...
5
votes
0answers
125 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
75 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, ...