Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

The tag has no usage guidance.

5
votes
1answer
92 views

Topology/Space of Recursive Algebraic Datatypes

I have a recursive algebraic datatype. I (somewhat arbitrarily) defined one function to compute distance between instances, and am trying to define a function to approximate a "vector" between ...
3
votes
1answer
71 views

Stream fusion in total functional language

As I understand, stream fusion consists in converting operations on lists to operations on streams (colists), optimize redundant codata to data and back conversions, fuse operations on streams, and ...
13
votes
1answer
230 views

What makes a language (and its type-system) capable of proving theorems about its own terms?

I've recently attempted to implement Aaron's Cedille-Core, a minimalist programming language capable of proving mathematical theorems about its own terms. I've also proven induction for λ-encoded ...
6
votes
1answer
80 views

Can all structurally recursive functions be written without explicit recursion using a catamorphism/fold?

In particular, I am thinking of a function which involves conditionals changing the recursive behavior and multiple F-algebras. ...
4
votes
0answers
436 views

Is it possible to derive induction by extending CoC with recursion?

Suppose we extended the CoC with primitive recursion; that is, we added a term µ x . t such that equality allowed unrolling recursive terms: ...
8
votes
1answer
130 views

Type for “ways values can be different”

I am looking for a concept in type theory that I am sure has probably been explored, but do not know the name behind. Let's consider a ML-like language with product and sum types and a Hindley-Milner ...
0
votes
0answers
271 views

Can $f^{2^N}(x)$ be computed in polynomial time when $f$ is linear?

Linear functions: definition Let's define a linear function as one expressible as an untyped λ-calculus term with the added restriction that no lambda argument can be used twice. Linear functions: ...
1
vote
0answers
36 views

Is it possible to use arbitrary fixpoint values on EAL without losing strong normalization?

From this question, the answerer states EAL-based languages can use arbitrary fixpoint types without losing strong normalization, because their normalization (and complexity) properties comes from ...
6
votes
1answer
82 views

Can you assign a type to any term of the λEA-calculus?

The untyped language of System-F and similar is the λ-calculus. That language has terms that can't be typed on System-F, λx.(x x) λx.(x x) being the most obvious ...
2
votes
1answer
289 views

Wouldn't the calculus of constructions with linear types be a simple functional core that is consistent and expressive?

I have recently asked if there is a simple functional core that is consistent and expressive. In another question, cody pointed out that this is an open problem to have a language that is: Consistent/...
15
votes
0answers
232 views

Are there simple core languages which are consistent and expressive?

The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, ...
6
votes
1answer
101 views

Programming language supporting infinitary rewriting of regular term graphs?

Do any practical programming languages support term graph rewriting of infinite but regular terms? For example the toy language CoCaml [1] supports computations on infinite regular streams. Coq ...
6
votes
4answers
450 views

Purely(ish) functional data structure with fast append and forward iteration

I find I have need for a data structure with a specific set of requirements: It represents an immutable sequence of values (fixed sized integers if this matters) Appending a new value to the end (and ...
15
votes
2answers
357 views

(How) Could we discover/analyze NP problems in the absence of the Turing model of computation?

From a purely abstract math/computational reasoning point of view, (how) could one even discover or reason about problems like 3-SAT, Subset Sum, Traveling Salesman etc.,? Would we be even able to ...
14
votes
1answer
999 views

Why do functional programming languages require garbage collection?

What's stopping ghc from translating Haskell into a concatenative programming language such as combinatory logic and then simply using stack allocation for everything? According to Wikipedia, the ...
2
votes
0answers
108 views

Is there is an intuitive explanation why call-by-name PCF is less expressive than both call-by-value PCF and lazy PCF?

J.C. Mitchell cites in his "Expressive power of programming languages" the result in Riecke's "Fully abstract translations between functional languages" about the call-by-value, call-by-name and lazy ...
1
vote
1answer
101 views

Observational Equivalence of open terms in PCF

The notion of observational equivalence is rather intuitive, but formally I'm having some doubts in the particular case of open terms. Lets consider the simple case where the terms ...
-3
votes
1answer
241 views

Can we say that Church encoding is a form of Gödelization?

We see here the following statement about Godelization: Gödel numbering in computer science means more or less "source code" and "data in binary format", so I hope the significance of this should ...
1
vote
0answers
50 views

Best Asymptotic Complexity for Persistent Union Find

In this paper https://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf, they claim to have a practically fast persistent union-find data structure for most use-cases, but it's still not polylogarithmic ...
7
votes
1answer
276 views

What type system fits the subclass of λ-terms that can be reduced optimally?

There is a subset of λ-calculus terms that can be reduced by Lamping's Abstract Algorithm without using the Oracle. That is an interesting subset, because only for those terms it is proven that ...
1
vote
0answers
39 views

Efficient compilation of interaction combinators with infinite cell types to usual interaction combinators?

It is known that interaction combinators can implement any interaction net system efficiently. Now, let us define a modification of interaction combinators, which, instead of two types of fan cells, ...
1
vote
1answer
130 views

Is the topsort from “Structuring Depth-First Search Algorithms” guaranteed to be (reverse) stable?

In "Structuring Depth-First Search Algorithms in Haskell", implemented in Data.Graph in the Haskell standard library, an algorithm for topologically sorting graphs is given: ...
-1
votes
2answers
577 views

How to implement a functional programming language efficiently?

Thanks to Petr and Andrej for their feedback. I'm rephrasing my question and give a bit of a context: Functional programming languages are mostly based on lambda calculus. Implementing a functional ...
10
votes
1answer
530 views

How do you encode Lamping's abstract algorithm using interaction combinators?

Interaction combinators have been proposed as a compile target for the λ-calculus before. That paper implements the full λ-calculus. It is also known that it is possible to optimize interaction-net ...
7
votes
1answer
160 views

Is it possible to unambiguously read back λ terms from interaction nets without node types?

A class of lambda terms can be evaluated using Lamping's abstract algorithm - that is, converting them to interaction nets and applying a set of rules. In order to get the result, you have to read ...
3
votes
1answer
99 views

Is there a pair of different lambda terms in the normal form that behave identically when applied to any input?

Let f and g be lambda terms in the normal form, such that f is intensionally different from <...
13
votes
2answers
411 views

Category theory and parsers — references wanted

Since I'm interested in parsers (mainly in parser expression grammars), I'm wondering if there's some work that gives a categorical treatment of parsing. Any reference on applications of category ...
10
votes
1answer
209 views

Type systems preventing laziness-related memory leaks?

Perhaps the main source of performance problems in Haskell is when a program inadvertently builds up a thunk of unbounded depth - this causes both a memory leak and a potential stack overflow when ...
3
votes
0answers
291 views

Distributive law between monads in Haskell

A distributive law between monads must satisfy laws that are usually given in terms of the units $\eta$ and multiplications $\mu$ of the two monads. Among the four laws there are: $\mu^S T \circ S l \...
6
votes
0answers
605 views

Is there a purely functional vector with O(1) access to the front and back but O(log n) concatenation?

Context: For fun and perhaps for actual use, I'm making my own programming language that would compile to Typed Racket, a statically-typed Lisp dialect. One of the major features I want to implement ...
3
votes
2answers
108 views

Typechecking liveness properties of coprograms

Clarification: in Total Functional Programming terminology, a program terminates with useful input, while a coprogram doesn't necessarily terminates, and repeatedly produces useful input. I am ...
0
votes
1answer
62 views

Can we design our own `if` clause in Normal Order evaluation

I have been reading SICP and have been thinking over a thing for quite some time related to evaluation using Substitution with ...
6
votes
0answers
130 views

Purely functional uniquely-represented deques

There are a number of purely functional deques that support $O(1)$ operations at each end. None that I know of are "uniquely represented" - deques with the same number of items can have different ...
4
votes
2answers
225 views

Can programming help one understand constructive mathematics?

I have read about the principles of constructive mathematics, for example, the principle of excluded middle is not allowed, and now I want to do some exercises to increase my understanding of the ...
24
votes
5answers
2k views

Are there any annotated formal verification systems for pure functional programming languages?

ACSL (Ansi C Specification Language), is a specification for C code, annotated with special comments, that allows C code to be formally verified. I have not looked into it, but I imagine that the ...
9
votes
2answers
634 views

Explaining monad transformers in categorical terms

Most resource regarding categorical notions in programming describe monads, but I've never seen a categorical description of monad transformers. How could monad transformers be described in the terms ...
6
votes
0answers
218 views

Generalizing Haskell: could we replace Hask with Cat?

N.B. I asked the same question on Stack Overflow but it was suggested that it is too theoretical for this forum. It is great that Haskell allows us to walk around in the category $Hask$. But ...
5
votes
2answers
235 views

Isomorphism between algebraic data-types

I have two types of trees in Haskell, defined as the least solution of the following equations: $T_1(A) \cong 1 + A + T_1(A) \times T_1(A)$ $T_2(A) \cong 1 + A \times T_2(A) + T_2(A) \times T_2(A)$ ...
4
votes
1answer
333 views

How can the actor model be applied to allow pure functional languages to have side-effects?

I just read this blog post which argues that monads might be too obscure or difficult to understand as the default "interface to the impure world" in purely functional programming languages; instead, ...
7
votes
1answer
188 views

Are there stronger notions of equivalence over lambda terms than beta equivalence?

I should add the context that I am concerned with strongly normalizing systems like System-F. I have what I consider a very strong notion of equivalence for lambda terms that goes something like the ...
3
votes
0answers
213 views

Is there any system where function equality (extensionality) is decidable?

Is there any programming language or system where function equality (extensionality) is decidable?
8
votes
0answers
358 views

Complete combinator basis for System F-omega

The S and K combinators form a complete (and Turing complete) basis when untyped. Within the Hindley-Milner type-system, and I believe within system $F$ as well, S and K can encode any well-typed ...
3
votes
1answer
150 views

A curious Wilf equivalence class of function compositions

I was enumerating pairs of functions from a size $n$ set into itself, and ran into these three relations which all generate the same integer sequence starting at index zero: 1, 1, 6, 87, 2200, 84245. ...
3
votes
1answer
805 views

Terminology for f(g(x)) = g(f(x))

There is a paper by Ritt from 1923 that calls the relation, $f(g(x)) = g(f(x))$, permutable functions. Is there a more recent terminology used in the literature, or is this still the standard?
10
votes
1answer
551 views

Algorithm to determine function equality on the simply typed lambda calculus?

We know that beta-equality of simply typed lambda-terms is decidable. Given M,N:σ→τ, is it decidable whether for all X:σ, MX $≃_β$ NX?
10
votes
1answer
384 views

What exactly does “semantically observable” side-effect mean?

I have question regarding pure functions. According to the Wikipedia page one of the requisites for a pure function is : Evaluation of the result does not cause any semantically observable side ...
9
votes
3answers
449 views

Is the class of primitive recursion functionals equivalent to the class of functions which Foetus proves to terminate?

Foetus, if you have not heard of it, can be read up on here. It uses a system of 'call matrices' and 'call graphs' to find all 'recursion behaviors' of recursive calls in a function. To show that a ...
18
votes
1answer
780 views

What are the practical issues with intersection and union types?

I'm designing a simple statically typed functional programming language as a learning experience. It appears that the type system I have implemented so far could (with a little extra work) ...
9
votes
3answers
1k views

How to make the Lambda Calculus strong normalizing without a type system?

Is there any system similar to the lambda calculus that is strong normalizing, without the need to add a type system on top of it?
6
votes
2answers
944 views

What is higher-order in higher-order abstract syntax?

I understand that using higher-order abstract syntax essentially means using host (meta) language abstraction facilities to represent binders in embedded (object) language. But, Why exactly is it ...