Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [typing]

type systems of programming languages

4
votes
1answer
124 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 ...
3
votes
0answers
37 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
104 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
46 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
42 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
64 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
68 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 ...
-1
votes
2answers
685 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
91 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
158 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
879 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
91 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
77 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
77 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
35 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
91 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 ...
17
votes
1answer
3k 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
62 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
135 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
57 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
117 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
111 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
191 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
397 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
65 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
61 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
116 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
356 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
152 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),...
2
votes
1answer
318 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
1k 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
314 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
265 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
1k 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
460 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
148 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
1k 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
358 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
866 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
527 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
284 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
165 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
400 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 ...
7
votes
2answers
340 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 ...
18
votes
3answers
1k 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 ...
19
votes
2answers
590 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$ ...