verifying that a variable, expression or value has the declared type

learn more… | top users | synonyms

2
votes
0answers
16 views

Is the strictly positive condition in Coq and Agda an aproximation?

Languages like Coq and Agda enforce that their inductive types occur "strictly positively" in their definitions. That is, the type should not occur to the left of an arrow of an argument of a ...
7
votes
0answers
113 views

Why do we have to forbid non-conforming lower and upper type bounds?

(it's a repost of my unanswered question from scala-user@googlegroups.com about Scala) In the Scala Language Specification, §4.4 Type Parameters, there is a requirement: The most general form of ...
4
votes
2answers
38 views

Algorithmic type checking for Calculus of Inductive Constructions

So from reading "Advanced Topics in Types and Programming Languages" (ATTPL) I know of the calculus of constructions (CoC). It also presents the "algorithmic" type checking rules. Reading Coq's ...
1
vote
0answers
8 views

Importance of indexes in Type(i) in calculus of inductive constructions [duplicate]

So I am reading about the calculus of inductive constructions. And I see here and here that there hidden indexes that the user does not know about in the $Type$ sort. It says that they are ...
7
votes
1answer
84 views

What is a non-contrived example of static type-checking being too conservative?

In Concepts in Programming Languages, John Mitchell writes that static type checking is necessarily conservative (overly strict) because of the Halting Problem. He gives as an example: ...
3
votes
0answers
61 views

Updating types during type inference in a Hindley-Milner type system

I'm looking at implementing type inference for a Hindley-Milner type system, and before I have even started to implement the Damas-Milner algorithm, while working through some examples, I hit some ...
3
votes
2answers
47 views

Definition of a size of type

In B. Pierce's book "Types and Programming Languages", he talks about the size of types (see pictures below). I searched the book for a definition but could not find one. I only found a definition ...
10
votes
1answer
226 views

Why aren't we researching more towards compile time guarantees?

I love all that is compile time and I love the idea that once you compile a program a lot of guarantees are made about it's execution. Generally speaking a static type system (Haskell, C++, ...) seems ...
0
votes
1answer
33 views

Type checking relation to logic

I am learning logic and functional programming and there is a topic called Type checking and their relationship to logic , I am unable to find any source that can help me in understanding this topic. ...
4
votes
3answers
65 views

Is there a technique for statically checking that a function is only called at a particular rate?

I was reading this article about types, and started wondering how static type checkers could enforce other properties in programs. For example, say I wanted to create a language which would allow ...
12
votes
2answers
45 views

What are potential pitfalls with having a minimal kernel that runs managed code?

Suppose I want to build an operating system based on a very small native lower kernel that acts as a managed code interpreter/runtime and a larger upper kernel compiled to a non-native machine ...
3
votes
1answer
74 views

Meaning of type inference rule for abstraction in lambda-calculus

Below is a snippet about simply typed lambda-calculus from CS152: Programming Languages Lecture 9 | Simply Typed Lambda Calculus, on printed‑page 15, indexed 23. $$ \frac {\Gamma, x: \tau_1 \vdash e: ...
0
votes
0answers
34 views

Type inference example?

In my programming languages course we are reviewing type inference, i didnt get very well how to make this task. I all ready search at the bibliography of my course (PLAI by Shriram krishnamurthi) ...
1
vote
1answer
66 views

Can Java be accurately described as statically and dynamically typed?

Java seems to be categorized as a statically-typed language [1], but I'm wondering if it would be accurate to describe it as generally statically-typed but having some dynamic typing because of the ...
0
votes
2answers
90 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 ...
2
votes
0answers
85 views

Can type information be encoded in the untyped lambda calculus?

I'm going to take the few pieces of knowledge I have about lambda calculi and ask a pair of very uninformed questions :-) Is it possible to "embed" the corners of the lambda cube within the untyped ...
0
votes
1answer
36 views

Type checking on assignment

I want to develop an interpreter. In the language, you have values and variables and types. The literals (the values) belong to some basic type. The subtypes can constrain the range of values. The ...
4
votes
1answer
57 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 ...
2
votes
3answers
236 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 ...
5
votes
1answer
362 views

Is it possible to do Dependent Types in Typed Racket?

Is it possible to use Dependent Types in the existing Typed Racket implementation? (ie do they exist in it?) Is it reasonably possible to implement a Dependent Types System using Typed Racket?
0
votes
1answer
67 views

What is a preterm parser?

I am working with HOL-Light parser and keeping seeing references to preterm parser. What is a preterm parser? The most informative statement I find is from the HOL-Light reference for the ...
3
votes
0answers
209 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 ...
3
votes
1answer
77 views

ML - Type Interface

From my recitation class - Can you please explain why does operator $"+"$ signature is $ int \rightarrow (int \rightarrow int)$ ? How does this graph is build ? And what is mean $t=u ...
8
votes
1answer
693 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 ...
11
votes
1answer
302 views

Type inference with product types

I’m working on a compiler for a concatenative language and would like to add type inference support. I understand Hindley–Milner, but I’ve been learning the type theory as I go, so I’m unsure of how ...
9
votes
2answers
927 views

Type-checking algorithms

I am starting a personal bibliographic research on type-checking algorithms and want some tips. What are the most commonly used type-checking algorithms, strategies and general techniques? I am ...