# Tag Info

50

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 ...

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 ...

37

Yes, sure. Many typed lambda calculi accept only strongly normalizing terms, by design, so they cannot express arbitrary computations. But a type system can be anything you like; make it broad enough, and you can express all deterministic computations. A trivial type system that encompasses a Turing-complete fragment of the lambda calculus is the one that ...

36

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 ...

35

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 ...

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 ...

29

[Note: this paragraphs is now outdated.] The title of your question contains an unwarranted assumption, namely that programming languages are "based on foundations of mathematics". This is generally not the case, although the two areas do have important relationships. A more accurate statement would be that (some) programming languages were designed using ...

29

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 ...

25

In most type systems, the type rules work together to define judgements of the form: $$\Gamma\vdash e:\tau$$ This states that in context $\Gamma$ the expression $e$ has type $\tau$. $\Gamma$ is a mapping of the free variables of $e$ to their types. A type system will consist of a set of axioms and rules (a formal system of rules of inference, as Raphael ...

25

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 programs ...

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

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

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\}$ . Notice that fully ...

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

$\to_\beta$ is the one-step relation between terms in the $\lambda$-calculus. This relation is neither reflexive, symmetric, or transitive. The equivalence relation $\equiv_\beta$ is the reflexive, symmetric, transitive closure of $\to_\beta$. This means If $M\to_\beta M'$ then $M\equiv_\beta M'$. For all terms $M$, $M\equiv_\beta M$ holds. If $M\... 20 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 ... 19 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 ... 18 Historically, the term "strongly typed programming language" came into use in the 70's in reaction to the existing widely used programming languages, most of which had type holes. Some examples: In Fortran, there were things called "COMMON" storage areas, which could be shared across modules, but there were no checks to see if each module was declaring the ... 18 The expressive completeness of the typed combinators compared to the simply typed lambda calculus has been demonstrated. For each untyped combinator, one needs a whole family of typed combinators. For example, one has$\mathbf{I}_{\alpha\to\alpha}\mathbf{K}_{\alpha\to(\beta\to\alpha)}\mathbf{S}_{\alpha\to(\beta\to\gamma)\to(\alpha\to\beta\to(\alpha\...

18

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 ...

17

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 ...

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

I just want to explain why intersection types are well-suited to characterize classes of normalization (strong, head or weak), whereas other type systems can not. (simply-typed or system F). The key difference is that you have to say: "if I can type $M_2$ and $M_1→M_2$ then I can type $M_1$". This is often not true in non-intersection types because a term ...

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 \$\...

15

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, ...

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