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.
741
questions
2
votes
1answer
266 views
Why does higher-order abstract syntax need an inverse to define catamorphisms?
In the introduction to the colorfully-named Boxes Go Bananas: Encoding Higher-Order Abstract Syntax with Parametric Polymorphism, Washburn and Weirich describe a problem in traditional formulations of ...
1
vote
0answers
8 views
Do forward chaining (Rete) business rules (Drools, ILOG) / production rules support higher order rules and compositionality?
There is this talk http://andrewcropper.com/pubs/jelia19-typed.pdf about higher order Prolog, about use of higher-order predicates (that takes other predicates as arguments) and compositionality of ...
2
votes
1answer
46 views
I don't see why the array[1..3, 1…2] is faster to index than array[1…2, 1…3]?
In my programming concept class we learned that for the array type it's faster to index in memory if the length of an element is = $2^n$. This case make us only need to offset instead of actually ...
0
votes
0answers
9 views
Manage nested recursions in the design of a concatenative language interpreter
I'm in the designing of an interpreter for a stack based concatenative language, and I'm currently stuck with a problem about recursion of some of my concatenative program to calculate factorial:
<...
0
votes
0answers
10 views
Is there any series of videos in which all the main algorithms are discussed without going into things like time complexity and steps [closed]
The course should be discussed in c language.
I am presently learning basic computer programming through a book and while doing the questions from the book from a chapter say array, I found out most ...
-1
votes
0answers
26 views
Why some languages are popular on Rosettacode but not elsewhere [closed]
I find that some languages are very popular on Rosettacode but not elsewhere. Following is the list from that site:
...
0
votes
0answers
14 views
Do Rank-1 (prenex) polymorphism and Predicative polymorphism mean the same?
https://en.wikipedia.org/wiki/Parametric_polymorphism says:
Rank-1 (prenex) polymorphism
In a prenex polymorphic system, type variables may not be instantiated with polymorphic types.[4] ...
0
votes
0answers
14 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. ...
3
votes
2answers
114 views
What can't you do without Turing-completeness?
I suppose that, since a Turing-complete language can simulate a Turing-machine, a non-Turing-complete language can't, but most programs do not have the simulation of a Turing machine as their purpose.
...
0
votes
0answers
15 views
What are the relations between these two descriptions of let polymorphism?
In Types and Programming Languages by Pierce, there are two descriptions of let-polymorphism.
Sec23.8 Fragments of SystemF on p359 says
This has led to various proposals for restricted fragments ...
0
votes
0answers
11 views
What are the difference and relation between type checking and type reconstruction?
In Types and Programming Languages by Pierce,
ML-style let-polymorphism was first described by Milner (1978). A num-
ber of type reconstruction algorithms have been proposed, notably the clas-
...
-1
votes
1answer
40 views
What is “Hindley-Milner (i.e., unification-based) polymorphism”?
In Types and Programming Languages by Pierce, Ch11 Simple Extensions extends the typed lambda calculus.
Section 11.5 Let Bindings says:
In Chapter 22 we will see another reason not to treat let as ...
2
votes
0answers
16 views
Does Hindley-Milner refer to the unification algorithm for type reconstruction, a type system, or a form of polymorphism?
What does Hindely-Milner refer to?
In Types and Programming Languages by Pierce, I only find that Section 22.4 Unification mentions "Hindley" and "Milner", when introducing the unification algorithm.
...
2
votes
1answer
42 views
Can most programs (except the IO part) be re-written as a sequence of matrix operations?
I got this idea recently. If we do not consider the data IO part of software, imagine the data is in the memory and we need to come out with some decision (which product to recommend to a user, how to ...
0
votes
1answer
21 views
Advantage of Stack-Based Allocation for Local Variables
While learning stack allocation, I came across this paragraph in the textbook (Programming Language Pragmatics - 3rd Edition):
Even in a language without recursion, it can be advantageous to use a ...
0
votes
1answer
23 views
What does valid method overriding mean?
In Types and Programming Languages by Pierce, from p257 to p258, about featherweight Java,
The predicate override(m, D, C→C0) judges whether a method
...
1
vote
2answers
48 views
Which is a type of objects in mainstream OO languages: a class, an interface, an abstract class, a metaclass?
In Types and Programming Languages by Pierce, Section 18.6 Simple Classes in Chapter 18 Imperative Objects says:
We should emphasize that these classes are values, not types. Also we can,
if we ...
0
votes
1answer
46 views
Is JavaScript a homoiconic language?
I can't help but notice the uncanny resemblence JavaScript has to LISP. JSON (JavaScript Object Notation), for instance, is a data structure that can be reconstituted into an object by subjecting it ...
2
votes
0answers
19 views
When did our current concepts of program modularity develop?
I take it that the concept of a modular subroutine call/return existed prior to the concept of a call stack (and hence to the possibility of recursive subroutines or of recursion limits). I would ...
1
vote
1answer
22 views
Does an ADT have multiple or only one representations/implementations?
Section 24.2 in Types and Programming Languages by Pierce defines ADTs in existential types:
A conventional abstract data type (or ADT) consists of (1) a type name A, (2) a concrete representation ...
0
votes
1answer
19 views
Why can System F1 a.k.a. λ → have kind `*`, but no quantification `∀`?
In Types and Programming Languages by Pierce, on p461 in Section 30.4 Fragments of Fω
30.4.1 Definition: In System F1 , the only kind is ...
-1
votes
1answer
42 views
What order logic does a system correspond to under Curry–Howard correspondence?
In Types and Programming Languages by Pierce,
Section 9.4 Curry–Howard correspondence on p109 has a table
Does the table mean that the simply typed lambda calculus ...
0
votes
0answers
9 views
Can two type expressions in different kinds have subtyping relation and equivalence relation?
In Higher-order bounded quantification ($F^ω_{<:}$), introduced in Ch31 in Types and Programming Langauges by Pierce, its subtyping and equivalence rules are:
Does subtyping relation only exist ...
0
votes
0answers
29 views
Is `→` a type operator?
In Types and Programming Languages by Pierce,
The level of types contains two sorts of expressions.
First, there are proper
types like Nat, Nat→Nat, Pair Nat Bool, and ∀X.X→X, which are ...
0
votes
0answers
23 views
Does λ→ have type operators?
In Types and Programming Languages by Pierce, Ch11 Simple Extensions introduces λ→ as the simply
typed lambda calculus with simple extensions, and introduces <...
0
votes
0answers
20 views
Is the language “untyped arithmetic expressions” in Types and Programming Languages not Turing complete?
In Types and Programming Languages by Pierce, is it correct that
the language introduced in Chapter 3 Untyped Arithmetic Expressions is not Turing complete? Because it doesn't provide recursion.
the ...
0
votes
0answers
14 views
How can we directly reaching inside and looking at the state of a partially existential object?
Types and Programming Languages by Pierce says in Section 26.5 Bounded Existential Types, about partial existential objects implemented in terms of bounded existential types:
We can make a similar ...
0
votes
0answers
24 views
What are the differences and relations between a type constructor and a type operator?
What are the definitions of a type constructor and a type operator?
What are their differences and relations?
I think a type operator is a function whose parameters are n types and return is a type. A ...
0
votes
1answer
42 views
How can an existential type be defined in terms of universal type?
In Types and Programming Languages by Pierce, how does the following achieve the definition of an existential type in terms of universal type, by polymorphic version of Church encoding of pairs?
...
0
votes
1answer
56 views
Why are ADT packages opened immediately after they are built, while existential objects opened as late as possible?
Section 24.2 in Types and Programming Languages by Pierce defines ADTs in existential types:
A conventional abstract data type (or ADT) consists of (1) a type name A, (2) a concrete representation ...
0
votes
1answer
56 views
How can mainstream OO languages support strong binary operations by classes?
Section 24.2 in Types and Programming Languages by Pierce compares ADT and existential objects,in terms of how well they support strong binary operations:
Other binary operations cannot be ...
0
votes
1answer
38 views
Are type abstraction values and universal types not for non functions, but only for functions?
In Types and Programming Languages by Pierce, Chapter 23 Universal Types has a summary of System F in the following figure, in particular, "type abstraction values" and their types "universal types".
...
0
votes
0answers
43 views
Why algebraic semantics of programming languages have died out and have not used today?
Algebraic semantics is one type of semantics that uses algebraic expressions for connecting the formal descriptions of initial and final states of some operation of some operation that is defined in ...
0
votes
0answers
25 views
Mutually contradicting rules in Prolog
What will happen in a Prolog program, if I set two rules/facts which contradict each other..
will it go with the rule/fact that appears first.. or it will show an error?
0
votes
1answer
36 views
How does this allow list operations to be applied to lists with elements of any type?
In Types and Programming Languages by Pierce, Chapter 11 is simple extensions of the simply typed lambda calculus with any simple base types. Section 11.12 introduces Lists.
How does the section ...
1
vote
1answer
21 views
What does it mean that a let-binding can be treated polymorphically, only if its right-hand side is a syntactic value?
Types and Programming Languages by Pierce says:
22.7 Let polymorphism
A final point worth mentioning is that, in designing full-blown
programming languages with let-polymorphism, we need to ...
0
votes
1answer
25 views
What is the purpose of erasing a type application to a term-application in parametric polymorphism?
From Types and Programming Languages by Pierce
23 Polymorphism
23.7 Erasure and Evaluation Order
in a full-blown programming language, which may include side-
effecting features such as ...
1
vote
2answers
94 views
Can we always transform a set of lines to a function?
If I have n lines in a programming language like Python (globally or inside a function):
...
0
votes
0answers
15 views
Languages with Static Upper Bounds for Resource Consummations
For Topics related to Blockchains and Smart Contracts, I'm developing a programming language that has the property that it is possible to calculate an upper bound on the consumed resources of a ...
0
votes
1answer
24 views
Does a term being normalizable mean the same as the term has a normal form?
From Types and Programming Languages by Pierce
A term $t$ is in normal form if no evaluation rule applies to it—
i.e., if there is no $t'$ such that $t -→ t'$.
and
A term $t$ is typable (or ...
0
votes
1answer
65 views
Do the following concepts belong to syntax or semantics?
I am not very sure about the difference between syntax and semantics.
Does each of the following concepts belong to syntax or semantics?
terms
values: terms that are possible final results of ...
1
vote
1answer
16 views
Do determinacy of one-step evaluation and uniqueness of normal forms apply to all (or most) languages in TAPL?
In Types and Programming Languages by Pierce, when talking about untyped arithmetic expressions in Chapter 3, there are two theorems:
$-→$ is single-step evaluation relation:
3.5.4 Theorem [...
1
vote
1answer
25 views
Does Types and Programming Languages use a recursive equation to define a recursive type or its generator?
In Types and Programming Languages by Pierce et al:
The recursive equation specifying the type of lists of numbers is similar to the equation specifying the recursive factorial function on page 52:
...
-2
votes
1answer
28 views
4
votes
0answers
47 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
...
0
votes
0answers
56 views
Converting Turing machine into the source code in industrial programming language?
Are there methods how to convert Turing machine (e.g. neural Turing machine or other rigorous Turing machine) into the source code/program that is written in some industrial programming language like ...
0
votes
0answers
14 views
In normative order evaluation, is there distinction between call by value, call by reference, call by sharing, etc?
Consider different ways of evaluating a procedure call and its arguments.
Essentials of Programming Languages says
All the parameter-passing mechanisms (natural parameter passing, call by value, ...
2
votes
0answers
16 views
How can we convert between a program using `call/cc` and a program using functions written in CPS?
The Scheme Programming Language says
It turns out that any program that uses call/cc can be rewritten in CPS without call/cc, but a total rewrite of the program (sometimes including even system-...
0
votes
0answers
13 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 ...
8
votes
1answer
453 views
Representation of the concatenation at the type level
I would like to learn more about concatenative programming through the creation of a small simple language, based on the stack and following the concatenative paradigm.
Unfortunately, I haven't found ...
