The tag has no wiki summary.

learn more… | top users | synonyms

3
votes
0answers
49 views
+50

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 ...
2
votes
1answer
116 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
761 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?
7
votes
1answer
158 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?
9
votes
1answer
81 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 ...
7
votes
3answers
191 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 ...
10
votes
1answer
178 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) ...
4
votes
3answers
225 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?
4
votes
2answers
160 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 ...
1
vote
0answers
67 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 ...
2
votes
1answer
106 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 ...
1
vote
2answers
178 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
285 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 ...
0
votes
0answers
38 views

What are some properties of the function that computes the ratio of the first N Jot programs that halt?

Let S(N) be a set of the first N programs in Jot. Suppose that F is function that returns an approximation of the ratio of programs in a set that halt (we can guess ...
10
votes
1answer
320 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 ...
1
vote
3answers
214 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
114 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 ...
-2
votes
8answers
340 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?
5
votes
1answer
221 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
2answers
355 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 ...
0
votes
1answer
183 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 ...
4
votes
1answer
253 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 ...
8
votes
2answers
586 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 ...
7
votes
1answer
373 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 ...
5
votes
2answers
147 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 ...
7
votes
2answers
179 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 ...
6
votes
2answers
154 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 ...
9
votes
2answers
559 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 ...
10
votes
1answer
425 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 ...
9
votes
1answer
280 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 ...
11
votes
1answer
1k 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 ...
3
votes
1answer
238 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 ...
14
votes
1answer
502 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, ...
3
votes
3answers
248 views

Automatic proofs or model checking in an extremely simplified functional language

Imagine a stripped down functional programming language, that has the following properties The only value type is an integer There are no side effects Functions are defined as a single expression, ...
4
votes
3answers
527 views

What are the relationships between Functional Reactive Programming, Automatic Differentiation, Self-Adjusting Computation and Partial Evaluation?

Self-adjusting computation seems to be related to all of the other topics, but I would like to get a clearer sense of how they all relate. For example, do any of them subsume or obsolete any of the ...
-6
votes
1answer
304 views

What function has the signature $ A \times \left ( B + C \right ) \rightarrow \left ( A \times B \right ) + \left ( A \times C \right ) $?

$ A \times \left ( B + C \right ) $ is isomorphic to $ \left ( A \times B \right ) + \left ( A \times C \right ) $, right? That means there's a function from one to the other and another function ...
10
votes
2answers
548 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
0answers
318 views

What is the origin and meaning of the phrase “Lambda the ultimate?”

I've been messing around with functional programming languages for a few years, and I keep encountering this phrase. I understand what lambda means, the idea of an anonymous function is both simple ...
-6
votes
3answers
283 views
6
votes
1answer
275 views

Implications of the rule of cumulativity in the Calculus of Constructions

Please help me understand some type theory research. As suggested in "Type Checking with Universes" by Robert Harper and Robert Pollack, we can add the following rule to our otherwise standard COC or ...
5
votes
2answers
268 views

With equirecursive types are there downsides to making all types potentially recursive?

By this I mean to ask, is it a bad idea to have all type constructor term expressions abstracted with $\mu$ just in case they need to be recursive? For example, $Bool : Type;$ $Bool = (\mu Bool' ...
6
votes
1answer
128 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 ...
11
votes
3answers
1k 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 ...
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
2answers
150 views

Automated transformation into spigot algorithm?

Is there any research on transforming 'standard' algorithms into spigot algorithms? I'd be happiest with automated transformations, but happy to learn about any research in this area. For my ...
8
votes
1answer
283 views

Functional Sparse-Matrix with good performance?

While writing a Petri Net program, I was faced with a choice about data structures to represent the graph. Adjacency lists (i.e. lists enumerating the arcs into and out of individual places or ...
9
votes
1answer
2k 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 ...
13
votes
2answers
869 views

Purely Functional Equivalent of B-Tree?

I am exploring the idea of writing a DBMS in purely functional way. The traditional data structure used for indexing is B-Tree. I'd like to know some purely functional equivalent of B-Tree that would ...
15
votes
4answers
639 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 ...
4
votes
1answer
337 views

Confluently Persistent String Data Structure

I'm looking for a confluentially persistent data structure for a string - so far I'm looking at finger trees. That is, how would I resolve two edits to the same base tree, and would I be able to ...