Skip to main content

Questions tagged [typing]

type systems of programming languages

Filter by
Sorted by
Tagged with
0 votes
2 answers
48 views

Types and programming languages: strange term construction?

Pierce's Types and Programming Languages has the following definition of terms: $$S_0=\emptyset$$ $$S_{i+1} = \{true,false,0\} \cup \{succ(t), pred(t),iszero(t)|t \in S_i\} \cup\{if(t_1)then (t_2)...
Hank Igoe's user avatar
  • 179
2 votes
1 answer
100 views

What is "invariants of the code"?

The Wikipedia page for strong and weak typing says: "Strong typing" generally refers to use of programming language types in order to both capture invariants of the code What is "...
robertspierre's user avatar
1 vote
1 answer
120 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 ...
Gaslight Deceive Subvert's user avatar
4 votes
1 answer
337 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 ...
Rafael Castro's user avatar
5 votes
1 answer
146 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-...
Kazark's user avatar
  • 253
4 votes
2 answers
462 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 ...
MiragePV's user avatar
4 votes
2 answers
86 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 ...
LambdaBeta's user avatar
2 votes
1 answer
51 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 ...
Murad Babayev's user avatar
4 votes
1 answer
81 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. ...
iambicSam's user avatar
5 votes
0 answers
100 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 ...
paulotorrens's user avatar
2 votes
5 answers
6k 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 "... ...
fredrik's user avatar
  • 31
5 votes
1 answer
125 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 ...
Alexis King's user avatar
5 votes
1 answer
233 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 ...
feersum's user avatar
  • 313
3 votes
2 answers
2k 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 ...
Chapi's user avatar
  • 55
1 vote
0 answers
116 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?
盛安安's user avatar
  • 944
2 votes
1 answer
166 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 ...
Tim's user avatar
  • 4,945
-1 votes
1 answer
148 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, ...
Tim's user avatar
  • 4,945
2 votes
1 answer
56 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 ...
Steven Maude's user avatar
0 votes
1 answer
164 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 ...
madcrazydrumma's user avatar
63 votes
14 answers
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 ...
effeffe's user avatar
  • 741
26 votes
1 answer
6k 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 ...
Alex R's user avatar
  • 473
2 votes
1 answer
116 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 ...
Lord Cat's user avatar
  • 143
3 votes
3 answers
216 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 ...
Ankur's user avatar
  • 628
2 votes
0 answers
74 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 ...
Robin Green's user avatar
1 vote
1 answer
163 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 ...
jhegedus's user avatar
  • 255
0 votes
1 answer
207 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 ...
Telastyn's user avatar
  • 499
4 votes
1 answer
327 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: ...
Hibou57's user avatar
  • 233
1 vote
0 answers
44 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 ...
luser droog's user avatar
5 votes
1 answer
85 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 ...
Bakuriu's user avatar
  • 807
4 votes
2 answers
85 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 ...
Theodore Murdock's user avatar
1 vote
1 answer
162 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 ...
Ellen Spertus's user avatar
4 votes
1 answer
728 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 ...
azrosen92's user avatar
  • 143
1 vote
2 answers
190 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),...
Guy Coder's user avatar
  • 5,101
3 votes
1 answer
485 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 ...
Aaron's user avatar
  • 131
14 votes
1 answer
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 ...
Juan's user avatar
  • 765
2 votes
1 answer
585 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 ...
Juan's user avatar
  • 765
4 votes
2 answers
375 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 ...
BlueBomber's user avatar
  • 1,297
9 votes
2 answers
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?
hawkeye's user avatar
  • 1,199
3 votes
1 answer
878 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 ...
babou's user avatar
  • 19.5k
2 votes
1 answer
205 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: <...
Michael's user avatar
  • 175
2 votes
2 answers
3k 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? ...
lal's user avatar
  • 121
4 votes
1 answer
393 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 ...
Artem Pelenitsyn's user avatar
7 votes
3 answers
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 ...
Martin Berger's user avatar
5 votes
1 answer
656 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 ...
edA-qa mort-ora-y's user avatar
3 votes
1 answer
313 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 ...
maaartinus's user avatar
6 votes
1 answer
179 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 ...
Dave Clarke's user avatar
  • 20.2k
11 votes
1 answer
559 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 ...
justkris's user avatar
  • 211
8 votes
3 answers
476 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 ...
Gilles 'SO- stop being evil''s user avatar
19 votes
3 answers
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 ...
Gilles 'SO- stop being evil''s user avatar
22 votes
2 answers
933 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$ ...
user avatar