Questions tagged [functional-programming]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
10
votes
1answer
755 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 ...
3
votes
1answer
123 views
13
votes
2answers
564 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
237 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 ...
7
votes
2answers
198 views

Prior work on finding domain-theoretic suprema of equivalent total functions?

In slightly more down-to-earth terms, this question is sort of about lazy evaluation in functional programming - except that it's more ambitious in general than just seeking what a typical Haskell ...
4
votes
1answer
394 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, ...
3
votes
0answers
417 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 \...
7
votes
0answers
724 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
137 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
72 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 ...
25
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 ...
6
votes
0answers
188 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
259 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 ...
12
votes
2answers
612 views

Continuation passing transform of binary functions

Recall the continuation passing transform (CPS transform) which takes $A$ to $\beta A \mathrel{{:}{=}} R^{R^A}$ (where $R$ is fixed) and $f : A \to B$ to $\beta f : \beta A \to \beta B$ defined by $$\...
6
votes
0answers
256 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
367 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)$ ...
7
votes
1answer
340 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
285 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
418 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
151 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. ...
10
votes
1answer
798 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?
3
votes
1answer
836 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?
11
votes
1answer
537 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
630 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 ...
22
votes
1answer
1k 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?
7
votes
2answers
1k 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 ...
2
votes
0answers
149 views

Evaluation contexts: outside-in vs inside-out

I heard that there exist two styles to define an evaluation context: outside-in and inside-out. Can someone give the definitions? Why are they so named (inside-out and outside-in)? What is the ...
3
votes
1answer
325 views

Learning road map for functional programming from the viewpoint of category theory

I am now considering about studying functional programming from the viewpoint of category theory. There are a lot of books about functional programming and category theory, I want some suggestions ...
14
votes
3answers
604 views

Associative hash mixing

Consider the lowly singly-linked list in a purely functional setting. Its praises have been sung from the mountain tops and will continue to be sung. Here I will address one among its many strengths ...
1
vote
2answers
223 views

Using partial functions to prove correctness

I'm interested in proving that a program (which may or may not terminate) will give the correct answer if it terminates. Given: $P$ is a family of programs, parameterized by a function $f$. Write $...
1
vote
3answers
622 views

Is there an array structure that allows for O(1) complexity for reverse, zip, slice etc operations?

Many operations on arrays have $O(n)$ complexity. If we represent arrays as accessors methods, many of them could be done in $O(1)$. For example, the $i$th item in the reverse of an array $A$ of ...
1
vote
3answers
347 views

“lambda” term usage in programming

could any one please let me know what is the relation between "lambda" and anonymous functions in programming? in other words why we say lambda function to an anonymous function? I am here trying to ...
1
vote
1answer
250 views

A few questions about ISWIM

I recently read Landin's paper "The Next 700 Programming Languages". But I was a bit confused by ISWIM. In particular, are functions first-class objects in ISWIM? It seems not because every ...
5
votes
2answers
713 views

Formal representation of algorithm using recursive algebraic data types

I have an algorithm written in Haskell which I am describing in my thesis. In the code for the algorithm I have a recursive data type similar to this: data Data = A Int | B Data | C Data Now I am ...
-1
votes
1answer
223 views

Newbie question: Meta-functions?

Consider a function F that takes a function and produces a function based on structure of the input function. As an example consider F that takes all functions having at least two conditionals and ...
5
votes
1answer
379 views

Is there any work on purely functional approximation algorithms?

It seems to me that approximating a solution to an NP-hard problem would be especially hard for the functional programmer. For example, graph problems are commonly NP-hard. But graphs are ...
5
votes
2answers
294 views

Why do we need PAP (partial aplication) objects in heap?

In the paper “Making a Fast Curry: Push/Enter vs. Eval/Apply for Higher-order Languages” by Simon Marlow and Simon Peyton Jones it is told that a PAP heap object may be created in the push/enter model ...
5
votes
2answers
627 views
8
votes
2answers
263 views

Resumption-based IO systems?

I've been playing around with resumptions lately, mostly from Abramsky's classic paper Retracing Some Paths in Process Algebra. They are quite slick (basically solutions to the domain equation $R = I \...
9
votes
1answer
474 views

What are possible implementations of Haskell's type classes and what are their (dis)advantages?

As far as I know, a Haskell function with type classes constraints is internally compiled to a function with additional arguments that receive dictionaries with the necessary implementations of each ...
12
votes
2answers
700 views

What are the relations between Alternative, MonadPlus(LeftCatch) and MonadPlus(LeftDistributive)?

Following up What’s an example of a Monad which is an Alternative but not a MonadPlus?: Assume $m$ is a monad. What are the relations betweem $m$ being an Alternative, a MonadPlusCatch and a ...
19
votes
2answers
3k views

What are the limits of total functional programming?

What are the limitations of total functional programming? It is not Turing-complete, but still supports a large subset of the possible programs. Are there important constructs that you could write in ...
15
votes
1answer
1k views

A mathematical (categorical) description of type classes

A functional language can be viewed as a category where its objects are types and morphisms functions between them. How do type classes fit in this model? I assume we should only consider those ...
36
votes
8answers
2k views

Higher-order algorithms

Most of the well-known algorithms are first-order, in the sense that their input and output are "plain" data. Some are second-order in a trivial way, for example sorting, hashtables or the map and ...
10
votes
2answers
1k views

How do I choose a functional dictionary data structure?

I've read a bit about the following data structures: Bagwell's Ideal Hash Tries Larson's Dynamic hash tables Red-Black trees Patricia trees ...and I'm sure there are a lot of others out there. I've ...
53
votes
2answers
6k views

What are the outstanding questions in purely functional data structures?

This question is inspired by another question about what's new in PFDS since the publication of Okasaki's book in 1998. I'll start with two questions I have: Is there a purely functional set data ...
3
votes
1answer
390 views

What can the Haskell package category-extras be used for?

See here. Has anyone attempted to use this to verify category theoretic proofs? Given the relationship between categories and graphs, are there some applications with respect to graph algorithms? What ...
29
votes
1answer
1k views

Programming languages with canonical functions

Are there any (functional?) programming languages where all functions have a canonical form? That is, any two functions that return the same values for all set of input is represented in the same way, ...
18
votes
4answers
972 views

How are imperative languages more different from each other than functional languages?

I'm reading Simon Peyton Jones's The Implementation of Functional Programming Languages and there's one statement that surprised me a little bit (on page 39): To a much greater extent than is the ...