type systems of programming languages

learn more… | top users | synonyms

3
votes
1answer
51 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: ...
1
vote
0answers
66 views

How does one guarantee that the commutative, associative and distributive properties hold for a type?

While most main stream programming languages allow for user defined types that can have the following properties: associative commutative distributive the only way I know of that this can ...
0
votes
0answers
7 views

How to apply the unification algorithm to a racket function

In my programming languages course we are reviewing unification algorithm by hand. The TA can't solve some examples of how to apply the unification algorithm to the ...
1
vote
0answers
16 views

Extending the type scheme for Burks/Warren/Wright machine to handle operators on functions?

Some background: Burks, Warren and Wright published a description of simple interpreter for a Logic Machine for unparenthesized Lukasiewicz notation (paper, SO question, c implementation, postscript ...
3
votes
0answers
22 views

Is dependency analysis required in order to type a program?

I have seen stated in various places that in order to allow an "increase in polimorphism" functional depency analysis should be performed, and type inference should be used for every declaration group ...
3
votes
0answers
33 views

Is there a term for the common semantics of global variables, static local variables, and fields?

I'm working on a graph representation of software for a static analysis project, and I'm finding a distinction that I have no name for between different types of variables. On one side of the ...
1
vote
1answer
49 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 ...
2
votes
1answer
53 views

What is the Inversion Lemma

I am taking a programming languages course, and we have had to use the Inversion Lemma many times in our proofs of preservation. We have been given the Inversion Lemma in each of these examples, but ...
0
votes
2answers
74 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
73 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 ...
7
votes
1answer
129 views

Why will the Hindley-Milner algorithm never yield a type like t1 -> t2?

I'm reading about this algorithm while writing an implementation, and see that, as long as every variable is bound, you'll always get either atomic types or types where the arguments will determine ...
2
votes
1answer
77 views

Would adding recursive named functions to Simply typed lambda calculus make it Turing complete?

Say I have Simply typed lambda calculus, and add an assignment rule: <identifier> : <type> = <abstraction> Where ...
1
vote
2answers
81 views

If dynamically typed languages are truly statically typed, unityped languages, what is the (finite) type expression of the one type?

Some claim that dynamically typed languages are in reality statically typed, unityped languages. This would imply to me that this one type should be expressible as a static, finite type expression, so ...
2
votes
1answer
198 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?
3
votes
1answer
130 views

Language independent software libraries

When trying to decide on the choice of a programming language for a specific task, people will often tell me: "use this language because it has the best library for the type of problems you are ...
2
votes
1answer
39 views

How is the following ML Curry expression evaluated

This question is not homework but it's related to material in a general course I take about programming languages, so I don't know whats the site policy about this In ML the following expression: ...
2
votes
2answers
282 views

Handling untrusted string input in printf in C [closed]

I stumbled upon the MSDN Best Practices for Code Review. Under the section “Untrusted Inputs”, I found following which I didn't understand properly. Why is the following considered safe? ...
3
votes
1answer
178 views

Scala as a language for Generic Programming

I posted the same Q at programmers.SE, but nobody really helps. In the paper “An Extended Comparative Study of Language Support for Generic Programming” by Garcia et al. an interesting comparison of ...
7
votes
3answers
297 views

Inheritance, and dynamic access to members/attributes and methods in Java-like languages

I have a question about inheritance in Java-like OO programming languages. It came up in my compiler class, when I explained how to compile methods and their invocation. I was using Java as example ...
5
votes
1answer
171 views

Algorithm for type conversion / signature matching

I'm working on an expression typing system and looking for insights on what algorithms may be available which solve my problem -- or a proof that its complexity is too high to be reasonable to ...
3
votes
1answer
196 views

Is the type inference here really complicated?

There's a question on SO asking why in Java the right type doesn't get picked in a concrete case. I know that Java can't do it in such "complicated" cases, but I'm asking myself WHY? The (for ...
6
votes
1answer
145 views

Efficient subtype testing

Languages like Java, C#, Eiffel, and C++ have subtype hierarchies which are directed acyclic graphs, due to interfaces in Java and C# and multiple inheritance in Eiffel and C++. An obvious way to ...
10
votes
1answer
222 views

Constraint-based Type Inference with Algebraic Data

I am working on an expression based language of ML genealogy, so it naturally needs type inference >:) Now, I am trying to extend a constraint-based solution to the problem of inferring types, based ...
6
votes
2answers
174 views

ML functions from polymorphic lists to polymorphic lists

I'm learning programming in ML (OCaml), and earlier I asked about ML functions of type 'a -> 'b. Now I've been experimenting a bit with functions of type ...
12
votes
2answers
341 views

ML function of type 'a -> 'b

Our professor asked us to think of a function in OCaml that has the type 'a -> 'b i.e. a function of one argument that could be anything, and that can return ...
13
votes
2answers
245 views

Are universal types a sub-type, or special case, of existential types?

I would like to know whether a universally-quantified type $T_a$: $$T_a = \forall X: \left\{ a\in X,f:X→\{T, F\} \right\}$$ is a sub-type, or special case, of an existentially-quantified type $T_e$ ...