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

learn more… | top users | synonyms

3
votes
2answers
30 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 ...
7
votes
0answers
164 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
28 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
57 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 ...
11
votes
2answers
24 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
58 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
31 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
54 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
85 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
80 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
34 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
53 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
227 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 ...
3
votes
1answer
267 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
57 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
158 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
74 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
604 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
275 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
824 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 ...