Questions tagged [functional-programming]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
9
votes
4answers
904 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 ...
1
vote
0answers
89 views

Kleisli-like category for applicatives?

I am wondering if there is a good way to complete the following analogy: monad : Kleisli category :: applicative functor : ?? That is, a given monad T on a ...
7
votes
2answers
815 views

Free theorems, where?

I've found this webapp which lets you generate a free theorem for a given type. The generated theorems quantify over types and relations on these types. These theorems (formulas) are theorems of which ...
2
votes
0answers
67 views

$[[ \text{fn} \ x => [x]^1]^2 [ \text{fn} \ y => [y]^3]^4]^5$ calls the identity function $\text{fn} \ x => x$ on the argument $\text{fn} \ y => y$?

This is question is related to this past question. I am currently studying the textbook Principles of Program Analysis by Flemming Nielson, Hanne R. Nielson, and Chris Hankin. Chapter 1.4 Constraint ...
1
vote
1answer
106 views

Phonology and lambda calculus

I wonder whether there is any relationship between lambda calculus and phonology (study of phonemes). Specifically, how one would use the concepts of lambda calculus (typed or untyped) in the study of ...
1
vote
0answers
43 views

What is the time complexity of substitution algorithms(normalization by evaluation, explicit subtitution)?

I'm studying the substitution algorithms of lambda calculus. I think now I understand how they work, but I couldn't find any materials about their time complexity yet. This is what I've thought about ...
9
votes
8answers
6k views

What are the simplest turing-complete systems? [closed]

Lambda Calculus is very simple. Are there even simpler turing-complete systems? Which is the simplest of them all?
592
votes
6answers
120k views

What's new in purely functional data structures since Okasaki?

Since Chris Okasaki's 1998 book "Purely functional data structures", I haven't seen too many new exciting purely functional data structures appear; I can name just a few: IntMap (also invented by ...
4
votes
1answer
241 views

Areas of research and open problems in functional programming [closed]

What are the major areas of functional programming that require more research and development? For example, I know a lot of people are asking for dependent types in Haskell, and someone at my uni is ...
14
votes
1answer
2k 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 ...
3
votes
3answers
1k views

Is it possible to generate a collision free hash function from an equality function?

I'm wondering if it's possible to go from an arbitrary equality function: Eq :: (obj, obj) -> bool to an identity/collision-free hash function: ...
1
vote
0answers
198 views

How do computers check if two functions are the same?

To prove that two given functions are the same involves proving infinitely many statements. I wonder how to implement so that a computer can check such a statement? An easy example is the following: ...
6
votes
1answer
288 views

Fixed set of type constructors to simulate all intensional inductive families?

I'm wondering, are there small dependent calculi that can simulate a language with inductive families (that is, has a type isomorphic to each inductive family, at least as powerful of induction ...
6
votes
1answer
213 views
7
votes
3answers
333 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 ...
6
votes
2answers
519 views

What category are Tagless Final Algebras final In?

The Haskell and Scala community have been very enamored recently with what they call tagless final 'pattern' of programming. These are referenced as dual to initial free algebras, so I was wondering ...
7
votes
2answers
859 views

What logic correponds via Curry-Howard to a Monad?

According to Moggi's 1991 paper "Notions of computation and monads" one can represent monadic equational logic with the well known monad $(T, \eta, \mu)$ with T an functor and the two natural ...
3
votes
0answers
212 views

Is it possible to check equality of equi-recursive types, or recursive λ-terms?

Can we determine if two λ-terms are equal? Given two lambda terms, let's say they are equal if their (possibly infinite) Bohm trees are. Under this definition, for example, ...
7
votes
3answers
352 views

When a type is a value?

In functional programming and in the theoretical setting of the $\lambda$-calculus it is standard to consider a lambda abstraction $\lambda x.M$ as a value. In my understanding, the intuitive reason ...
6
votes
0answers
155 views

Immutable Space Model

I have heard it said that time is more precious than space because we can reuse space but not time. What if we treat space with this much reverence? What is generally known about models of ...
1
vote
0answers
85 views

A categorized (?) list of functional pearls in JFP and ICFP

Is there a list of (categorized preferred) functional pearls ever published in ICFP and JFP? I could go to the ICFP proceedings and JFP issues and find all of them, but this would be time-consuming. ...
5
votes
1answer
112 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
113 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 ...
12
votes
1answer
308 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
152 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
496 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: ...
15
votes
2answers
3k views

What is a zipper, and how does it relate to a tree-like structure?

I was reading a chapter in LYAH which didn't really make sense to me. I understand that zippers can arbitrarily traverse a tree-like structure, but I need some clarification on it. Also, can zippers ...
8
votes
1answer
159 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
285 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: ...
6
votes
1answer
98 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 ...
1
vote
0answers
44 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 ...
2
votes
1answer
573 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/...
7
votes
1answer
196 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 ...
14
votes
0answers
364 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, ...
17
votes
2answers
3k views

Category theory, computational complexity, and combinatorics connections?

I have been trying to read “Pearls of Functional Algorithm design”, and subsequently “The Algebra of Programming”, and there is an obvious correspondence between recursively (and polynomially) defined ...
5
votes
1answer
110 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
1answer
1k views

Trampoline that automatically balances heap and stack

While working through Fogus' Functional Javascript, I came across the trampoline function, which can be used to make safe recursive functions that don't blow up the stack. In Fogus' words, "Of course ...
5
votes
4answers
685 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
443 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 ...
2
votes
0answers
122 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
118 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
437 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 ...
1
vote
0answers
72 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 ...
16
votes
3answers
2k views

Bootstrapping a Finger Tree Structure

After working with 2-3 finger trees for quite a bit I have been impressed by their speed in most operations. However, the one issue I have run into is the large overhead associated with the initial ...
18
votes
2answers
2k views

What persistent data structure for a set of partially ordered elements?

I need to store sets of elements of type a. Type a is partially ordered, so comparing $a_1$ and $a_2$ can return smaller, greater, equal or incomparable. One problem with hashtables is that two equal ...
6
votes
1answer
323 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
1answer
167 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
vote
0answers
44 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, ...
46
votes
2answers
6k views

Explaining Applicative functor in categorical terms - monoidal functors

I'd like to understand Applicative in terms of category theory. The documentation for Applicative says that it's a strong lax ...
1
vote
2answers
1k 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 ...