New answers tagged

3

There has been a shift during the last 5-15 years in how editors and IDEs are built. It was recognized that IDEs have to perform a lot of the same tasks that compilers do. In fact, in order to support things like lexical highlighting, syntax highlighting, semantic highlighting, refactoring, warnings ("yellow squigglies"), errors ("red squigglies"), ...


0

I can only think of some uncurrying of 1 and 3. $\forall X. (X \times int) \rightarrow X$ It looks like we can not uncurry this one, unless we transform it first into the isomorphic type 1. $int \rightarrow \forall X. (X \times int) \rightarrow X$ Alternatively, if we can apply an isomorphism, (3) can be rewritten as $$ \forall X. int \rightarrow (X \times ...


2

Any Compiler, Interpreter, Assembler performs the task to encode the programming language into strings of binary instructions that the host system's processor could understand. No matter what high-level programming language you use, the programs needs to be converted into binary strings specific to the instruction-set of the processor. So on basis of my ...


6

A programming language is a formal language. Most likely its context-free, sometimes context-sensitive, rarely just regular (mostly eso-langs, and some assembly languages). There usually exists a formal grammar somewhere that defines the syntax of the language. Sometimes, this grammar isn't even written down explicitly and only exists inside the reference ...


7

You download the language's tools. If the language can be compiled to a "native" executable, (e.g., like "Rust") then you download the compiler, and probably a run-time support library, and maybe a linker, a debugger, etc. If the language requires an interpreter (e.g., like Ruby) or a "virtual runtime environment" (e.g., like Java) then you download those ...


13

A programming language is a formal language, informally speaking a collection of words with a well-formed set of specific rules. As such, you can write down the definition of a formal language and thus a programming language on a piece of paper. Also, if I've written down somehow digitally the definition of a programming language, surely you can represent ...


1

Microsoft has developed a practical code checker (whose name escapes me at the moment) which performs halt-testing. It exploits the fact that the code it checks is human-written and not arbitrary, just as you suggest. More importantly, it bypasses the impossibility proof by being allowed to return the answer 'Cannot decide' if it runs into code too ...


16

Languages that are guaranteed to halt have seen wide spread use. Languages like Coq/Agda/Idris are all in this category. Many many type systems are in fact ensured to halt such as System F or any of its variants for instance. It's common for the soundness of a type system to boil down to proving that all programs normalize in it. Strong normalization is a ...


2

The "single type" for Python is called "object" and described in https://docs.python.org/3/reference/datamodel.html: Objects are Python’s abstraction for data. All data in a Python program is represented by objects or by relations between objects. (In a sense, and in conformance to Von Neumann’s model of a “stored program computer”, code is also ...


1

You are able to distinguish between types in a type system, because you admit at least a universe of types, in within types exist (e.g. Product types, Sum types, etc...). On the other hand, if you have only one type in your universe, then it doesn't matter how you call it or what it is: is the only thing that exists, therefore you can't compare it with ...


1

In those bullets, Harper is addressing common misconceptions about static versus dynamic typing. Each of those bullet points starts with a misconception, and then continues with Harper's clarification. So, the first misconception is: Dynamic languages associate types with values, whereas static languages associate types to variables. Harper disagrees, ...


0

The value of $r$ at the end is $$ \sum_{i=1}^{n-1} \sum_{j=i+1}^n \sum_{k=1}^j 1 = \sum_{i=1}^{n-1} \sum_{j=i+1}^n j. $$ You take it from here. You can use a computer algebra system such as Wolfram alpha to help you with the calculations. If you are only interested in asymptotics, then you can use the following upper bound: $$ \sum_{i=1}^{n-1} \sum_{j=i+1}^...


3

Let us consider the LOOP programming language. For a program $f$, denote by $f_{\max}(n)$ the maximal value of a variable at the end of the program, given that initially, all variables are at most $n$. If $f$ has only one loop then $f_{\max}(n) = O(n)$. In contrast, using two nested loops you can compute the product function, and the resulting program $g$ ...


Top 50 recent answers are included