Questions tagged [programming-languages]

Questions related to design, implementation, and analysis of programming languages. NOT for questions about how to program, which are off-topic on this site.

170 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
13 votes
0 answers
220 views

Why do we have to forbid non-conforming lower and upper type bounds?

(it's a repost of my unanswered question from [email protected] about Scala) In the Scala Language Specification, §4.4 Type Parameters, there is a requirement: The most general form of a ...
Vladimir Reshetnikov's user avatar
11 votes
0 answers
165 views

Denotational semantics of object-oriented languages

I am interested in denotational semantics of object oriented languages. Namely, what are the common/typical denotations of objects used in the literature? Is this an interesting topic these days? The ...
zpavlinovic's user avatar
  • 1,654
10 votes
1 answer
192 views

Using naturality to prove $f: \forall\alpha. \alpha\times\alpha\to\alpha$ must be a projection

Suppose we have a System F term $f : \forall \alpha. \alpha\times\alpha\to\alpha$, interpreted in a parametric model which is a bicartesian closed category. I was wondering if in such context it is ...
chi's user avatar
  • 14.6k
9 votes
1 answer
827 views

Turing Machine-Like Formalism for The Actor Model

Turing machines have a formal symbol alphabet, state and transition-rules based description of how a computation is done. The Actor Model is sometimes mentioned as a more powerful computational-...
Adi Shavit's user avatar
7 votes
0 answers
136 views

Evolutionary theory applied to programming languages

I'm looking for books applying evolutionary theory to the history of programming languages. Researching the topic I have found an interesting paper - Modelling the Evolution of Programming Languages ...
polymechanos's user avatar
7 votes
0 answers
506 views

Is there any defined programming model for 'Self-Learning' NPUs?

Qualcomm is creating a Neuromorphic Processing Unit or an NPU called zeroth. IBM is also working on a brain inspired chip under Synapse program. Standford's Neurogrid might be a similar example. ...
xsnk's user avatar
  • 71
6 votes
0 answers
81 views

Can all computational complexity results be expressed in terms of programming languages?

Computational complexity results are often explained in intuitive terms as statements about the possible efficiencies of algorithms to solve certain classes of problems. However, on a more formal ...
glS's user avatar
  • 286
6 votes
0 answers
172 views

Is there relation between K-Framework and structural operational semantics?

K-framework strives to give one (instead of two - operational and denotational) semantics for industrial programming languages. The same unification is done by structural operational semantic as well. ...
TomR's user avatar
  • 1,401
6 votes
0 answers
898 views

Which programming languages have a syntax that can be described by deterministic context-free grammars?

This question asks which programming languages have a syntax that cannot be described by deterministic context-free grammars - the answer is "Many [...] including Algol 60, C, and C++". Until ...
user200783's user avatar
5 votes
0 answers
115 views

Which languages, if any, implemented parametric polymorphism before ML?

In particular, was there any kind of implementation at the time Christopher Strachey wrote Fundamental Concepts in Programming Languages? In that work, Strachey lists Ad Hoc and Parametric ...
itsbruce's user avatar
  • 224
5 votes
0 answers
354 views

Dennis Ritchie citation for "the C declarator syntax is an experiment that failed"?

I've often heard that the C declarator syntax described as "an experiment that failed." I've seen claims that this sentiment is also shared by its creator Dennis Ritchie. Does anybody have an actual ...
Paul J. Lucas's user avatar
4 votes
0 answers
66 views

Is there a computer language with optional dependent types?

I'm looking for a computer langauge with "dependent types" but... The problem with it having a full implementation is that you end up having to write formal type proofs to get even anything ...
zooby's user avatar
  • 263
4 votes
0 answers
249 views

How shall I understand the definitions of `let` expression?

let as used in programming languages is defined in lambda calculus as per https://en.wikipedia.org/wiki/Let_expression#Let_definition_defined_from_lambda_calculus ...
Tim's user avatar
  • 4,895
4 votes
0 answers
82 views

Scopes vs objects -- would a language make sense that voids the difference?

So there's this adage that says "Objects are a poor man's closures", which can equally well be reversed, which I understand to mean that they are equivalently expressive. What strikes me about the ...
Kelley van Evert's user avatar
4 votes
0 answers
224 views

PL: How can I prove the type of something using "Inversion for Typing"?

I'm currently going through this book about programming languages, and in section 4.2, Lemma 4.2 it says this: Lemma 4.2 (Inversion for Typing). Suppose that $\Gamma \vdash e : \tau$. If $e = \texttt{...
Reed Oei's user avatar
  • 203
4 votes
0 answers
191 views

Expression Problem: Why are simple parameterized types a non-solution?

I'm studying the expression problem at the moment and it seems like I'm missing something. I used a data-centered approach (i.e. OOP) as the basic setup and then introduced two type variables, one for ...
Bengt's user avatar
  • 141
4 votes
0 answers
141 views

Why can't a programming language be both fully recursive and polymorphic

In my theory of computation class last Spring my professor said in passing that a programming language cannot be both fully recursive and polymorphic. I didn't think much of it till now? What does it ...
Michael Chav's user avatar
4 votes
0 answers
77 views

Understanding a paper on polynomial recursion in all finite types

So I wasn't sure weather or not this counted as "research level" or not but I figured it wasn't so I decided to post it here. There is a paper by S. Bellantoni et al. called "Higher ...
Jake's user avatar
  • 3,810
4 votes
0 answers
120 views

Is there any research to indicate programmers are/are not moving to a hybrid of functional and object-oriented?

I am converting the OCaml Format module which does I/O and maintains state in a record with mutable values. As such it is a good candidate for me to convert to pure F#, pure C# and a hybrid. Since ...
Guy Coder's user avatar
  • 5,101
3 votes
0 answers
83 views

Formalize the proof of theorem 2.4 in Harper's PFPL

In Harper's Practical Foundations for Programming Languages, page 19, rule (2.9) defines the $sum$ function inductively. $$ \frac{b:nat}{sum(zero;b;b)}\tag{rule 2.9a} $$ $$ \frac{sum(a;b;c)}{sum(succ(...
gingerologist's user avatar
3 votes
1 answer
234 views

Is “x' = f(x)” a programming paradigm?

I'm the author of GateBoy (a gate-level simulation of the original Game Boy hardware) and Metron (a C++ to Verilog translation tool). One big issue I had to work around for both projects is the ...
tanjent's user avatar
  • 66
3 votes
0 answers
290 views

What is the runtime (time complexity) of Type Inference in Simply Typed Lambda Calculus?

I was told that the runtime of OCAML or Scala is EXPTIME - which seems really bad! However, since people use type inference (deciding the type of a term or program or expression) in practice - it must ...
Charlie Parker's user avatar
3 votes
0 answers
51 views

Is there a language which enforces "no escape" of variables?

Many languages with GC perform escape analysis to reduce heap allocations. Is there a language with a "no-escape" construct that tells the programmer during compile time to not escape ...
Olle Härstedt's user avatar
3 votes
0 answers
92 views

Semantics of "write-once" variables for complex data structures

Question My use case for what is described below is not a language or compiler implementation, but finding a reasonable semantics for this feature in a an abstract calculus. Ideally, you give me a ...
phipsgabler's user avatar
3 votes
0 answers
55 views

On the diamond property for $F_{\omega}$ in TAPL

In page 455, of Pierce´s TAPL and page 560, the single-step diamond property of reduction: $S \Rrightarrow S' \land T \Rrightarrow T' \implies \exists V. T \Rrightarrow V \land U \Rrightarrow V$ ...
user1868607's user avatar
  • 2,194
3 votes
0 answers
92 views

What is the first programming language where the keyword "new" appeared?

It's really interesting when this keyword first appeared as a lot of popular languages but relatively old languages( C++, C#, Java, JS ) use it. I understand use of "new" in C++ in practical manner( ...
Andrei's user avatar
  • 131
3 votes
1 answer
484 views

SICP: applicative or normal order evaluation

I'm trying to solve Problem 1.5 from SICP book. Consider the following definitions: (define (p) (p)) (define (test x y) (if (= x 0) 0 y)) (test 0 (p)) The ...
Attilio's user avatar
  • 255
3 votes
0 answers
87 views

Computability of Kolmogorov complexity in total languages

It is well known that the Kolmogorov complexity is uncomputable in Turing-complete programming languages. However, what about total programming languages? For example, is the Kolmogorov complexity of ...
xuq01's user avatar
  • 1,190
3 votes
0 answers
51 views

How do you resolve this paradox with the invariance theorem?

The invariance theorem of kolmogorov complexity states that for two different languages with complexity functions $K_1$ and $K_2$, we have $$\exists c.\forall s. K_1(s) \le K_2(s) + c$$ Here is an ...
Christopher King's user avatar
3 votes
0 answers
146 views

An instance when you can eliminate propositional double negation in coq

Suppose st: string -> nat and X stands for the string 'X'. Given the hypothesis ...
CuriousKid7's user avatar
3 votes
0 answers
52 views

Why interaction net languages use interaction rules to represent their syntaxes?

What I have looked up into: here, here and here What I have learnt: What is an interaction net, its deduction & interaction rules, How deduction rules can be changed into interaction rules -- ...
Bell Fox's user avatar
3 votes
0 answers
66 views

Query Langauge analogy to Turing Completeness

Is there a completeness property for query languages (like SQL, Cypher, Datalog, etc) that is analogous to Turing completeness in programming languages? I wondered if it is something like being able ...
Jason Kapp's user avatar
3 votes
0 answers
741 views

How to decide between operational, denotational, and axiomatic semantics?

Context I'm designing a language which implements lambda calculus and (first-order) predicate calculus, where lambdas behave as the abstraction encapsulating logic, compositionally forming a ...
Phizo's user avatar
  • 51
3 votes
0 answers
78 views

Definition of imperative semantic in a HDL context

I've been studying from this book the topic of "Synthesis and optimization of digital circuit". In chapter 3 some theory about programming languages is exposed. I was wondering what's the meaning of ...
user8469759's user avatar
3 votes
0 answers
162 views

Is there any programming system that enables reversible computations?

Better explained with examples, I need a programming system with the following characteristics: ...
dokkat's user avatar
  • 121
3 votes
0 answers
90 views

What happened to Active Databases?

When reading the literature on declarative programming technology. A particular technology that sounded promising is active databases. It essentially allows the programmer to specify rules about data ...
Arturo Hernandez's user avatar
3 votes
3 answers
2k views

“In object-oriented programming, the program is organized around its data”

In a description of OOP in my textbook, it is written that “in procedure oriented program the program is organized around its code while in object oriented programming, the program is organized around ...
MrAP's user avatar
  • 129
2 votes
0 answers
16 views

Does exist another models like CARDIAC, LMC and IPC?

I'm working with CARDIAC (Cardboard Illustrative Aid to Computation) that is a model created at Bell Labs in 1968 to explain students how the computers worked with the Von Neumann architecture to ...
Osvaldo Santos's user avatar
2 votes
0 answers
81 views

What are strong examples of programming languages whose type systems don't embed into their native type theory?

Given a typical popular programming language, its native type theory is a dependent type theory which describes invariants, preconditions, predicates, and other generalizations of typical type-system ...
Corbin's user avatar
  • 220
2 votes
0 answers
28 views

History of the category of effectful computations

The 1971 paper A Catalog of Optimizing Transformations contains this passage: irreducible subprograms require special handling. (An irreducible subprogram is one which maintains a history, performs I/...
Theo H's user avatar
  • 321
2 votes
0 answers
64 views

Do any industry programming languages use Martin-Löf style identity types?

Most programming languages have some kind of type systems but are there any programming languages widely used outside of academia (in consumer-oriented tech, finance etc.) that have intensional ...
kodi's user avatar
  • 21
2 votes
0 answers
47 views

Understanding the simulate of an IF loop program through a LOOP program

We have the following operation $\text{IF} \ x_i =0 \ \text{THEN} \ P \ \text{END}$. I want to simulate this using a $\text{LOOP}$ program. Here is what I have: $$\text{IF} \ x_i = 0 \ \text{THEN} \ P ...
Ski Mask's user avatar
  • 463
2 votes
0 answers
104 views

What's the meaning of linguistics?

In the programming language theory world, there are two important terminologies, i.e syntax, and semantics. I can understand these two terminologies: syntax is about sentence's structure (e.g. a valid ...
chansey's user avatar
  • 285
2 votes
0 answers
108 views

Compiling an impure language into a pure stack-based language

For a personal learning and fun project, I build an abstract virtual machine based on a stack. The instructions are simple and act on the top of the stack only. There are also stack operators such as <...
Foxy's user avatar
  • 255
2 votes
0 answers
33 views

Is Event Calculus applied for program verification?

Recently I've read wiki page about Robert Kowalski (Prolog author) and stumbled upon interesting concept of Event Calculus. The wiki article mentions only few applications of this logical language. I ...
M. Twarog's user avatar
  • 131
2 votes
0 answers
119 views

How does one program in a tag system?

I've played with 2-tag systems a bit and read all about tag/lag systems. They're great for experimenting with computation, and obviously useful as intermediaries in various proofs. My question is: ...
Trev's user avatar
  • 296
2 votes
0 answers
100 views

Are the permutation or weakening lemmas needed for term substitution?

In TAPL book, page 453, Pierce discusses the following lemma: $\Gamma , x:S , \Delta \vdash t:T \land \Gamma \vdash s:S \implies \Gamma, \Delta \vdash [x \mapsto s]t:T$ He claims that when $t$ is ...
user1868607's user avatar
  • 2,194
2 votes
0 answers
311 views

Proper algorithm for resolving ambiguity in grammars via enforcing associativity and precedence rules

I was told there is a algorithm that always resolves ambiguity for grammars that have issues with precedence and associativity. I know ambiguity in general is undecidable, so I only want to resolve ...
Charlie Parker's user avatar
2 votes
0 answers
37 views

When concatenating two sequences, can evaluations of two input sequences be in parallel with each other?

In Practical Foundation of Programming Languages by Harper (www.cs.cmu.edu/~rwh/pfpl/2nded.pdf), 37.3 Multiple Fork-Join So far we have confined attention to binary fork/join parallelism ...
Tim's user avatar
  • 4,895
2 votes
0 answers
109 views

What are the relation and differences between reification and type passing semantics?

https://en.wikipedia.org/wiki/Type_erasure says type erasure refers to the load-time process by which explicit type annotations are removed from a program, before it is executed at run-time. ...
Tim's user avatar
  • 4,895