# Tag Info

55

Idris is Turing Complete! It does check for totality (termination when programming with data, productivity when programming with codata) but doesn't require that everything is total. Interestingly, having data and codata is enough to model Turing Completeness since you can write a monad for partial functions. I did this, years ago, in Coq - it's probably ...

40

The main differences are along two dimensions -- in the underlying theory, and in how they can be used. Lets just focus on the latter. As a user, the "logic" of specifications in LiquidHaskell and refinement type systems generally, is restricted to decidable fragments so that verification (and inference) is completely automatic, meaning one does not require ...

39

For a rather simple version of dependent type theory, Gilles Dowek gave a proof of undecidability of typability in a non-empty context: Gilles Dowek, The undecidability of typability in the $\lambda\Pi$-calculus Which can be found here. First let me clarify what is proven in that paper: he shows that in a dependent calculus without annotations on the ...

38

In C, void is used for multiple unrelated things. Depending on what it's used for, its meaning may be a unit type, an empty type, or something else. When void is used by itself (as opposed to void*, a pointer to void), it's a unit type, i.e. a type with a single value. Functions that return void are said to “return nothing”, but what this really means is ...

34

To understand the difference between sets and types, ones has to go back to pre-mathematical ideas of "collection" and "construction", and see how sets and types mathematize these. There is a spectrum of possibilities on what mathematics is about. Two of these are: We think of mathematics as an activity in which mathematical objects are constructed ...

32

A type is a property of computations. It's what you write on the right-hand side of a colon. Let me elaborate on that. Note that the terminology isn't completely standard: some articles or books may use different words for certain concepts. A term is an element of an abstract syntax that is intended to represent computation. Intuitively, it's a parse tree. ...

32

The first thing to note is that this isn't necessarily true. For example, depending on the language a function with that type, besides being the identity function, could: 1) loop forever, 2) mutate some state, 3) return null, 4) throw an exception, 5) perform some I/O, 6) fork a thread to do something else, 7) do call/cc shenanigans, 8) use something like ...

32

Here, "values", "types", and "kinds" have formal meanings, so considering their common English usage or analogies to classifying automobiles will only get you so far. My answer pertains to the formal meanings of these terms in the context of Haskell specifically; these meanings are based on (though are not really identical to) the meanings used in ...

26

The question is somewhat problematic, since it relies on a subjective definition of "better." Dependently-typed languages such as Agda, Idris, and Coq have a stronger type system than Haskell. This means, you can use the types in these languages to prove strictly more properties about your code than in Haskell. That is, there are more incorrect ...

25

Let's have a go. I'll not bother about Girard's paradox, because it distracts from the central ideas. I will need to introduce some presentational machinery about judgments and derivations and such. Grammar Term   ::=   (Elim)   |   *   |   (Var:Term)→Term   |   λVar↦Term Elim   ::=   ...

23

Refinement types are simply usual types with predicates. That is, given that $T$ is a usual type and $P$ is some predicate on $T$ $$\{v:T \mid P(v)\}$$ is a refinement type. $T$ in this case is called a base type. AFAIK, in Liquid Haskell, they also allow some dependend function types, that is types $\{x:T_1 \to T_2 \mid P\}$ [1]. Notice that fully ...

23

It is a common misconception that we can translate let-expresions to applications. The difference between let x : t := b in v and (fun x : t => v) b is that in the let-expression, during type-checking of v we know that x is equal to b, but in the application we do not (the subexpression fun x : t => v has to make sense on its own). Here is an example: ...

22

Expanding my comment: Dependent types can type more programs. "More" simply means that the set of programs typable with dependent types is a proper superset of the programs typable in the simply-typed $\lambda$-calculus (STLC). An example would be $List_{2*3+4}(\alpha)$, the lists of length $10$, carrying elements of type $\alpha$. The expression $2*3+4$ is ...

21

The original Curry-Howard correspondence is an isomorphism between intuitionistic propositional logic and the simply-typed lambda calculus. There are, of course, other Curry-Howard-like isomorphisms; Phil Wadler famously pointed out that the double-barrelled name "Curry-Howard" predicts other double-barrelled names like "Hindley-Milner" and "Girard-Reynolds"...

20

If you know about the difference between sets and classes in set theory, then it may help to think about the matter as $$\mathrm{type} : \mathrm{kind} = \mathrm{set} : \mathrm{class}.$$ If not, you can think of kinds as "large" or "higher" types whose elements may be types, or may involve types in some fashion. For example: Bool is a type Type is a kind ...

19

The dependent sum is a common generalization of both the cartesian product $A \times B$ and the coproduct $A + B$. It just so happens that the HoTT book introduces dependent sum by generalizing $A \times B$, because that does not require the boolean type to be defined first. The coproduct is a special case of dependent sum. Given types $A$ and $B$, consider ...

19

First a terminological explanation: negative and positive positions come from logic. They are about an assymetry in logical connectives: in $A \Rightarrow B$ the $A$ behaves differently from $B$. A similar thing happens in category theory, where we say contravariant and covariant instead of negative and positive, respectively. In physics they speak of ...

19

On the left of the turnstile, you can find the local context, a finite list of assumptions on the types of the variables at hand. $$x_1:T_1, \ldots, x_n:T_n \vdash e:T$$ Above, $n$ can be zero, resulting in $\vdash e:T$. This means that no assumptions on variables are made. Usually, this means that $e$ is a closed term (without any free variables) having ...

18

Consider the finite multisets $\mathbf{Bag}\:X$. Its elements are given by $\{x_1,\ldots,x_n\}$ quotiented by permutations, so that $\{x_1,\ldots,x_n\}=\{x_{\pi 1},\ldots,x_{\pi n}\}$ for any $\pi\in\mathbf{S}_n$. What is a one-hole context for an element in such a thing? Well, we must have had $n>0$ to select a position for the hole, so we are left with ...

17

Some use cases for multiple type arguments include maps/dictionaries Map<K,V>, where you have one key parameter and one value parameter product types Pair<A,B> sum types, AKA variants Variant<A,B>, which represent a value which might be either of type A or of type B Function-like types Func<A,B> representing a function from A to B "...

17

One of the defining properties of the $\bot$ or empty type is that there exists a function $\bot \to A$ for every type $A$. In fact, there exists a unique such function. It is therefore, fairly reasonable for this function to be provided as part of the standard library. Often it is called something like absurd. (In systems with subtyping, this might be ...

16

Maybe a better question for somebody coming from set theory and grappling with how set theory and Martin-Löf type theory differ, is to reflect on what sets are. Your intuitions about set theory and the foundations of mathematics will be infected with unquestioned set-theoretic assumptions that you take for granted. Alas Martin-Löf type theory does not share ...

16

In the lambda calculus with no constants with the Hindley-Milner type system, you cannot get any such types where the result of a function is an unresolved type variable. All type variables have to have an “origin” somewhere. For example, the there is no term of type $\forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta$, but there is a term of type $\... 16 Dependent types are types which depend on values in any way. A classic example is "the type of vectors of length n", where n is a value. Refinement types, as you say in the question, consist of all values of a given type which satisfy a given predicate. E.g. the type of positive numbers. These concepts aren't particularly related (that I know of). Of course, ... 16 In traditional Martin-Löf type theory there is no distinction between types and propositions. This goes under the slogan "propositions as types". But there are sometimes reasons for distinguishing them. CoC does precisely that. There are many variants of CoC, but most would have $$\mathsf{Prop} : \mathsf{Type}$$ but not$\mathsf{Type} : \mathsf{Prop}\$. ...

16

Supplemental 2016-10-03: I mixed up induction-induction and induction-recursion (not the first time I did that!). My apologies for the mess. I updated the answer to cover both. I find the explanations in the Forsberg & Setzer's paper A finite axiomatisation of inductive-inductive definitions illuminating. Induction-recursion An inductive-recursive ...

15

The question under what circumstances we need to jump from a universe to one higher in the hierarchy is a good one. Having the hierarchy and the ability to climb it is important. You need to jump levels when you want to treat a universe as a type or as part of a type. For example to define functions of (non-dependent) type $$A \rightarrow \mathcal{U}_i$$...

15

First, I assume you've already heard of the Church-Turing thesis, which states that anything we call “computation” is something that can be done with a Turing machine (or any of the many other equivalent models). So a Turing-complete language is one in which any computation can be expressed. Conversely, a Turing-incomplete language is one in which there is ...

15

Category theory is not necessary to understand programming languages, it's not even necessary to do advanced research on programming languages. Most programming language people don't know (much) category theory. Category theoretical methods have been useful mostly in a small part of programming language research, namely in the analysis of functional ...

15

Type safety and type soundness are synonyms in most theoretical work. Type soundness is often formulated with respect to an operational semantics as (type) preservation and progress. Preservation states that if an expression has some type, then after a step of evaluation (via the operational semantics), the resulting expression can be given the same type. ...

Only top voted, non community-wiki answers of a minimum length are eligible