Podcast #128: We chat with Kent C Dodds about why he loves React and discuss what life was like in the dark days before Git. Listen now.

Questions tagged [pl.programming-languages]

Programming languages, in particular, focussing on their semantics.

Filter by
Sorted by
Tagged with
-1
votes
0answers
60 views

Dependent type theory where branching information informs typing derivations?

In Extensional Martin-Löf type theory (extended with the necessary types) I don't believe the following is derivable $$ x:\mathbb{N},\,rep:\varPi n:\mathbb{N}.Vec\,n\ \vdash Rec_{\mathbb{B},b.Vec\, x}\...
-1
votes
1answer
58 views

Chomsky-Schutzenberg Hierarchies explained for physicist (general) [closed]

I am classically trained in physics, however I have been interested in the use of information theory in studying some classical systems. As someone who is somewhat unfamiliar with the language of ...
7
votes
3answers
234 views

Can Non-termination be considered an algebraic effect?

Non-termination is sometimes considered an effect. I have been reading about algebraic effect systems (What is algebraic about algebraic effects and handlers?), and I suspect non-termination (like ...
5
votes
1answer
110 views

Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion?

To perform type inference in the presence of polymorphic recursion, one can use a Kleene-Mycroft iteration to compute the principal type of an expression. To type $\mathsf{fix}\ f\ldotp e$, we define $...
3
votes
1answer
107 views

Verified type checkers

Most of the work on programming language metatheory mechanization focus on the declarative properties of the languages (e.g., type soundness), but fail to address the algorithmic side, i.e. the type ...
9
votes
2answers
303 views

Applications of algebraic geometry in type theory/programming language theory

Lately, I have become interested in algebraic geometry and have started reading on it. I still know very little about this field, but I do want to know if it has any connection with my main field, ...
0
votes
1answer
157 views

Where does a C-like language without heaps belong in the automata hierarchy?

Assume that the language C', unlike C, has well-defined semantics, but has similar features: pointers and manual memory management through malloc and free. Assume that C'' is the same as C' without ...
9
votes
1answer
596 views

What is the “question” that programming language theory is trying to answer?

I've been interested in various topics like Combinatory Logic, Lambda Calculus, Functional Programming for a while and have been studying them. However, unlike the "Theory of Computation" which ...
0
votes
0answers
60 views

How to get started with program synthesis

I am a CS Major, I am a programmer with 10 years of experience. i want to get to know about program synthesis. there are no video tutorials / courses available online. i have researched about Emina ...
10
votes
2answers
204 views

Intuition Behind Strict Positivity?

I'm wondering if someone can give me the intuition behind why strict positivity of inductive data types guarantees strong normalization. To be clear, I see how having negative occurrences leads to ...
1
vote
0answers
43 views

How to justify this causally consistent execution in the $(vis, ar)$ framework for distributed consistency models?

In Figure 5.1 of the book "Principles of Eventual Consistency" by Sebastin Burckhardt, 2014, Causal Consistency (CC); wiki is (mainly) defined as the conjunction of $hb \subseteq vis$ and $hb \...
3
votes
2answers
220 views

Extending Hindley-Milner to type mutable references

I have been trying to implement a programming language from scratch, and have gotten reasonably far. It reads just like Python, other than the fact that let is used ...
1
vote
0answers
60 views

Confusion about the visibility and arbitration relations in a formal framework for distributed consistency models

In the POPL'14 paper "Replicated Data Types: Specification, Verification, Optimality" and the book "Principles of Eventual Consistency", the authors propose a formal framework for specifying ...
6
votes
1answer
262 views

How to tell if an effect is algebraic?

I've read Bauer's What is algebraic about algebraic effects and handlers? and he talks about IO being an algebraic effect, even though it doesn't have any equations. In other papers on algebraic ...
4
votes
0answers
85 views

Proof that CIC or Dybjer-style eliminators are strongly-normalizing?

Related to this question I'm wondering, what is the standard technique for showing that dependent types with eliminators are strongly normalizing? I'm thinking something like the Calculus of ...
5
votes
1answer
186 views

Is F<: with bottom undecidable?

We all know that F<: is undecidable: http://www.cse.chalmers.se/~abela/lehre/SS07/Typen/pierce93bounded.pdf However, I have difficulties finding that anyone claiming the version with bottom added ...
4
votes
0answers
130 views

Hereditary Substitution with Inductives and Eliminators?

I'm wondering, is there any existing work on hereditary substitution with inductive type families and dependent eliminators? In particular, normalizing the application of an eliminator to an ...
3
votes
0answers
141 views

Busy Beaver Equivalent for the Untyped Lambda Calculus

In the same way that the Busy Beaver function is defined for Turing Machines, we could define a similar function for the untyped lambda calculus: Over all terms in the ULC composed of ...
11
votes
2answers
319 views

Hereditary substitution with a universe hierarchy

I've read about hereditary substitution for the Simple Lambda Calculus and for The Logical Framework with distinct terms and types. I'm wondering, are there any examples of hereditary substitution in ...
5
votes
2answers
210 views

Typing of substitution in a bidirectional type system

In most typed lambda calculi, we have the following lemma: If $\Gamma \vdash t_1 : \tau_1$ and $\Gamma, x : \tau_1, \Delta \vdash t_2 : \tau_2$ then $\Gamma,\Delta[t_1/x] \vdash t_2[t_1/x] : \tau_2[...
5
votes
2answers
317 views

Preservation under Substitution with Telescopes

In the simply typed lambda calculus, one can show the following result, known as "preservation under substitution": If $\Gamma \vdash v : \tau_1$ and $(x : \tau_1) \vdash t : \tau_2$, then $\Gamma \...
6
votes
2answers
100 views

Formal semantics of tactics

Tactics are supposed to represent inference rules in a system, and it might seem unnecessary at first to formalize the semantics of tactics; nevertheless, modern theorem provers can have pretty ...
10
votes
1answer
442 views

Proof techniques for showing that dependent type checking is decidable

I'm in a situation where I need to show that typechecking is decidable for a dependently-typed calculus I'm working on. So far, I've been able to prove that the system is strongly normalizing, and ...
6
votes
3answers
214 views

Why/when do we ever need transfinite loop variants?

I do not understand why one would ever need a transfinite loop variant. Why do natural-number-valued variants not suffice? My simple (but perhaps too naive) argument is: if a loop $L$ terminates ...
11
votes
5answers
395 views

Representing bound variables with a function from uses to binders

The problem of representing bound variables in syntax, and in particular that of capture-avoiding substitution, is well-known and has a number of solutions: named variables with alpha-equivalence, de ...
5
votes
1answer
180 views

Confusion about a formal definition of PRAM consistency

I am reading the paper "Consistency in Non-Transactional Distributed Storage Systems" by Paolo Viotti and Marko Vukolić. The authors provide a comprehensive survey of various consistency semantics ...
5
votes
3answers
455 views

Sorting a programs instructions until it works

Lets say I have a computer program below. (define (factorial x) (if (= x 0) 1 (else (* x (factorial (- x 1))))) I then take each line of the ...
-1
votes
1answer
198 views

What is the practical importance of making or using a Turing complete language? [closed]

I get what a Turing machine is and what language is a Turing-complete language but when someone introduces me to a new programming language (like Solidity) and says it is Turing complete, what am I ...
5
votes
2answers
118 views

Does Standard ML validate (CBV) eta equivalence?

$\eta$ equality of functions is fundamental in their Category-theoretic semantics but in practice even "functional" languages include "impure" features that violate it. Note that this is not an issue ...
6
votes
3answers
3k views

Difference between syntax and semantic error in programming languages

When compilers generate errors for a specific programming language, there's distinction between syntax & semantic errors. E.g. ) + f 3 has ill-formed syntax, ...
8
votes
1answer
65 views

Question on subtyping of handlers in “An Effect System for Algebraic Effects and Handlers”

I had a question on subtyping in the paper "An Effect System for Algebraic Effects and Handlers". I was wondering why there isn't a subtyping rule for adding effects on both sides of a handler type, ...
3
votes
1answer
109 views

Escaping references in Eff and resources

In the paper "Programming with Algebraic Effects and Handlers" there is the issue where references (dynamic instances of a state effect, defined using algebraic effects) can propagate outside the ...
7
votes
1answer
245 views

Avoiding Cycles with Unification and Subtyping

Context I realize that subtyping often doesn't admit principle types, and that inference in the presence of subtypes is undecidable. I'm working in a context where typechecking should simply fail ...
2
votes
1answer
202 views

programming language with type-level functions

Is there any programming language out there that allows the same set of tools it offers, to be used at the type level as well? I know, Haskell and some other ML family languages allow parametric types ...
21
votes
2answers
2k views

Has the semantics of TeX (as a programming language) ever been formalized?

It seems to me that the macro language employed by $\TeX$ can maybe be seen as some kind of term rewriting system or some kind of programming language with call-by-name scoping. Even modern ...
17
votes
1answer
345 views

List of (unsolved) complexity problems arising from PL

What are some major, open computational complexity problems that arise from programming languages, especially program analysis and compilation? I am looking for problems on the lines of "the time ...
0
votes
1answer
112 views

Language/type system closest to Haskell without general recursion

I've implemented a completely functional DSL, and now I'd like to reason about it. It would be helpful to be able to compare it to existing languages. The type system is parametric polymorphic with ...
12
votes
3answers
432 views

Type-based memory safety without manual memory manage or runtime garbage collection?

Let's say we wanted a typeful, pure functional programming language, like Haskell or Idris, that is aimed at systems programming without garbage collection and has no runtime (or at least not more ...
2
votes
2answers
164 views

How can you state how abstract interpretation gets around Rice's Theorem succinctly?

At this question, abstract interpretation has a nice in-depth look. However, I'd like someone to clearly and very precisely state how abstract interpretation takes the result of Rice's Theorem over ...
1
vote
1answer
166 views

Algebraic effects and handlers, dynamic effects

What exactly are dynamic effects? What does it mean to dynamically create an effect? In a language with algebraic effects and handlers (such as Eff or Koka) one could already do different operations ...
2
votes
0answers
72 views

Categorical model of binding / first class modules

Binders are explained using presheaves (Pitts/Gabbay A new approach to Abstract Syntax with variable binding) What is the equivalent (categorical) theory to explain first class modules as in 1ML ?
1
vote
0answers
101 views

Definitions of strongest postconditions [closed]

The weakest precondition of while loop $\mathtt{while}(G)\{C\}$ with respect to postcondition $P$ can be characterized by the least fixed point of the predicate transformer $X ~\mapsto \neg G \wedge ...
4
votes
1answer
116 views

Questions about algebraic effects and handlers, decomposed handlers

Can a handler always be decomposed? Say a handler for Get and Set effects could be decomposed to a handler for Get and a handler for Set. After they could be composed again by first applying the ...
3
votes
2answers
212 views

Languages that lack contraction, weakening or exchange

When learning about generalized arrows, a question arised to me: Are there any languages (or potential languages) that lack one or more of the structural rules: contraction, weakeing and exchange? ...
2
votes
1answer
108 views

Is there a sense in which we can say error returned from a function is the reverse of context?

This came up in a discussion about golang, but I think it applies more generally. Context in which a function is executed (specially in when we have RPCs) and error returned from a function seem to ...
8
votes
2answers
1k views

What kind of theoretical object corresponds to a C++ concept?

I am lacking a background in theoretical computer science but I would have liked to understand to what kind of theoretical objects C++ concepts corresponds to. Basically, C++ concepts allow to define ...
2
votes
1answer
84 views

Completeness of Constraint Typing (type inference) question regarding $\sigma'$

The theorem of completeness of type inference states the following: Suppose $\Gamma \vdash t:S| _{\mathcal{X}}C$, ...
6
votes
0answers
142 views

Relationship between Pataraia's theorem and inductive-recursive definitions?

Pataraia's fixed point theorem gives a constructive proof of the fact that if you have a monotone function $f$ on a DCPO, then it has a least fixed point. I've frequently used this fixed point theorem ...
6
votes
1answer
175 views

Graph rewriting with one-to-many pattern matching?

In the single-pushout approach to graph rewriting, many nodes in a pattern graph can be matched to a single node of a target graph. My question is if there is a notion of graph rewriting where the ...
7
votes
2answers
140 views

What's the definition of join on iso-recursive types?

In languages with subtyping, there is often a "join" operation defined to compute the least upper bound of two types. It's used in type-checking, for example to find the smallest type that covers both ...