Questions tagged [typing]

type systems of programming languages

Filter by
Sorted by
Tagged with
0
votes
0answers
14 views

Can the value model for variables only be used together with static typing, not with dynamic typing?

There are two models of variables: the value model (e.g. variables in C) and the reference model (e.g. variables in Python). There is also a distinction between static typing and dynamic typing. Can ...
0
votes
1answer
41 views

Find typing derivation of STLC term with reference types

The problem is to find the typing derivation of a term of the call-by-value STLC extended with reference types. The evaluation and typing rules for this language is given in Types and Programming ...
4
votes
1answer
200 views

Typing rule for binding groups

In "Typing Haskell in Haskell", by Mark P. Jones, is provided a sort of haskell-like specification for typing Haskell. As stated in this paper, binding groups is a area "neglected in most theoretical ...
5
votes
1answer
82 views

Type system for Query DSL with only simple GADTs: what typing judgments are needed?

Background I have several F# codebases with reasonably high level of complexity of code. In order to convince myself that the code is solid I do whatever I can to write as much of it as possible type-...
3
votes
2answers
227 views

In Hindley-Milner system, how can I prove that let id=\x.x in id id is well-typed?

I am trying to infer the type and prove that this is well-typed: let $f =\lambda x.x$ in $f f$ Obviously the $f$ is the identity function, so it's the same as let $id =\lambda x.x$ in $id$ $id$ I ...
4
votes
2answers
66 views

Union of fixed and floating point types

Say I have two real number types. They may be floating or fixed point. How can I construct a new type whose values are at least the union of the two with the minimal number of bits? There are 3 cases ...
2
votes
1answer
45 views

Typing by value

I wondered if there was a generalized name for typing a variable by assigning a specific value to it. For instance a = 4 This would make the variable ...
4
votes
1answer
73 views

How is type safety handled differently between reference and value types?

I'm trying to understand how type safety is preserved for value types and for reference types, specifically in languages with managed memory (such as C#). I understand that reference types (i.e. ...
5
votes
0answers
84 views

How could one write typing rules with variables defined at call-site?

I'm trying to write typing rules for a simple language, which is basically a lambda calculus with SSA-like $\phi$-nodes, which basically exchange formal parameters for actual parameters. For ...
0
votes
3answers
3k views

What is a type definition?

When reading about data types, "type definition" is often used without any prior explanation to what it means. For example, in https://en.wikipedia.org/wiki/Type_system, we have the sentence "... ...
5
votes
1answer
103 views

Local type argument synthesis when type variable does not appear in arguments

I am implementing the techniques described in the classic Local Type Inference paper. Specifically, I am implementing the type argument synthesis algorithm from section 3. My algorithm seems to ...
5
votes
1answer
190 views

Polymorphism restriction on lambda-bound variables in HM

I'm trying to implement the Hindley-Milner type system, following Milner 1978, "A Theory of Type Polymorphism in Programming" (link). In the Hindley-Milner system, a polymorphic let-bound expression ...
2
votes
2answers
1k views

Lambda Calculus Type Inference

I'm currently trying to learn how to infer most general types on lambda calculus, and due to the lack of information on the subject I could find on Google I'm forced to attempt what I think is logical ...
1
vote
0answers
104 views

Typing rules of coinductive types?

Are there typing rules for specific coinductive types such as conat or stream, or even in general the M-types?
2
votes
1answer
101 views

Is type inference done by an interpreter static or dynamic?

Type inference can be done by a compiler, and in such cases, type inference is static. Type inference can also be done by an interpreter. An interpreter does the jobs of both compilation and ...
-1
votes
1answer
93 views

What concept is for a name referring to different types at different points in execution?

In programming language theory, which concept means that a name can refer to values of different types at different points of execution of a program, dynamic typing, implicit i.e. inferred typing, ...
2
votes
1answer
43 views

Identification and the definition of data type

A frequently cited definition of data type is that it is a set of values and a set of operations of those values. I've never read any mention along the lines of a type must be capable of being ...
0
votes
1answer
118 views

How does a language abstract away from underlying byte machines?

So as the title suggests, How does a programing language, such as Java or C, abstract itself away from underlying byte machines? Im curious, because I know that static/dynamic typing, data ...
64
votes
14answers
17k views

How can I explain to my parents that I study programming languages?

I am currently finishing my MSc in computer science. I am interested in programming languages, especially in type systems. I got interested in research in this field and next semester I will start a ...
20
votes
1answer
5k views

What are the major differences between row polymorphism and subtyping

I hear often that row-polymorphism is a better approach than subtyping, but I have difficulty finding anything comparing them in detail. I'm especially interested in the perspective of a user of the ...
2
votes
1answer
75 views

Confusion about data types, compilers, hardware data representation and static vs dynamic typing

I am trying to understand static vs dynamic typing, but am really struggling to see how everything fits together. It all starts with data types. As far as I understand, data types are quite abstract ...
3
votes
3answers
145 views

Isn't Domain of a variable nothing but a constraint?

In Constraint programming we have Variables and their Domains and then all the constraints, but if you at the concept of a domain of a variable it is nothing but another type of constraint, you are ...
2
votes
0answers
62 views

What is effect typing useful for when all global effects already have to be in the IO monad?

This paper adds effect handlers to a number of languages, including Haskell - and also adds a form of effect typing to Haskell. But what's the point of the latter? I know that effect types can be used ...
1
vote
1answer
127 views

Pierce's Types and Programming Languages : circular definition of terms?

In Pierce's book, on page 26-27 it is given a definition of terms for a simple language using inference rules. In the picture below it is marked by red highlighting the problematic part. What is ...
0
votes
1answer
125 views

Why are types and grammar non-terminals so distinct?

Sorry ahead of time if some of my terminology is inaccurate, my formal training isn't quite to the level it should be. Almost all programming languages with types separate built-in functions ...
4
votes
1answer
232 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
452 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 be ...
1
vote
0answers
33 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 ...
5
votes
1answer
73 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 polymorphism," functional dependency analysis should be performed, and type inference should be used for every declaration ...
3
votes
2answers
66 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
141 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 ...
3
votes
1answer
491 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 ...
1
vote
2answers
165 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 present),...
3
votes
1answer
376 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 ...
14
votes
1answer
2k views

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

I'm reading about the Hindley-Milner typing 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 ...
2
votes
1answer
412 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 ...
3
votes
2answers
302 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 ...
8
votes
2answers
2k 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
611 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
178 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
2k 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? ...
4
votes
1answer
374 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
1k 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
590 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
290 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
167 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 ...
11
votes
1answer
468 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 ...
8
votes
3answers
379 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 ...
19
votes
3answers
2k 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 ...
20
votes
2answers
693 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$ ...