Questions tagged [functional-programming]

Functional programming is a programming paradigm which primarily uses functions as means for building abstractions and expressing computations that comprise a computer program.

Filter by
Sorted by
Tagged with
5
votes
0answers
78 views

Difference between “functional programming languages” and “lambda calculus based languages”?

In "Can programming be liberated from the Von Neumann Style?", John Backus states: The main reason FP systems are considerably simpler than either conventional languages or lambda-calculus-based ...
5
votes
0answers
59 views

Can we simulate any dependent datatype with `Eq`?

Consider the canonical homogeneous equality type: Eq : (A : Set) -> A -> A -> Set, with constructor ...
5
votes
0answers
79 views

What are the properties of the unsided fold?

Foldl and folr are 2 very important functions for FP and Haskell, but I have never heard much about the unsided fold: fold f [a,b,c,d] = (f (f a b) (f c d)) That ...
4
votes
3answers
950 views

How can SML infer types like this?

Wikipedia says: fun factorial n = if n = 0 then 1 else n * factorial (n-1) A Standard ML compiler is required to infer the static type int -> int of this ...
4
votes
1answer
502 views

Why are dependently typed languages such as Agda used for proofs, if supercompilers for simpler typed languages can do the same?

Proof assistants such as Agda can be used to assert properties about programs, such as "the double of a number is even". Interestingly, supercompilers can be used for the same purpose, creating ...
4
votes
2answers
71 views

Is there a universal identity or zero value for folding?

I'm using Haskell notation for illustration, hopefully it is known widely enough for this to make sense. In the following fold function the second argument is what I'm calling the identity: ...
4
votes
1answer
422 views

Prove foldl fusion law

I have proven the foldr Fusion Law as follows: Given f is strict, f a = b and ...
4
votes
1answer
102 views

Writing the coherence conditions for a monad in a functional laguage

i recently asked a related question about the relationship between monads in category theory and Haskell. The answerer showed me the following classes and instances: ...
4
votes
1answer
280 views

How do you represent LISP as mathematical / logical model?

I asked this in stackoverflow, but the question probably fits here better. This question arose from the objection that LISP is regarded as a functional language with some simple principles, namely ...
4
votes
1answer
51 views

Description of lists with functions in LISP

I have been given the following implementation of basic list functions in LISP: ...
4
votes
4answers
10k views

What are differences between Static Scope and Dynamic Scope?

My teacher has provided the following pseudo-code, and says that the output using static scope is 1 2 3, but the output using dynamic scope is ...
4
votes
2answers
101 views

When does a type generalise another type?

In languages like Haskell, with a Hindley-Milner type system, when does a type $t$ generalise a type $u$? I use the definition: $t$ generalises $u$ iff $\forall\ v: v \text{ unifies with } u \...
4
votes
1answer
99 views

Why are there two not operators in lambda calculus?

From Wikipedia: $\mathrm{true} = \lambda a. \lambda b. a$ $\mathrm{false} = \lambda a. \lambda b. b$ Because true and false choose the first or second parameter they may be combined to ...
4
votes
1answer
278 views

Type Inference and Generalization

I've been trying to understand type inference for Hindley-Milner-based languages, and I'm struggling to understand how generalization works. Let's say I have the following program in Haskell: ...
4
votes
1answer
57 views

Inline caching in not object oriented languages

I've been recently studying inline caching as a technique to optimize method dispatch in object oriented languages. Basically, the idea is that one can remember what was previously dispatched and ...
4
votes
1answer
129 views

What is the name of this type of function composition?

If standard function composition is defined as: (define compose { (B → C) → (A → B) → (A → C) } F G -> (λ X (F (G X)))) What type of ...
4
votes
1answer
108 views

In what cases is graph rewriting not enough to avoid duplicate work?

As I understand, evaluating something like the following in normal order evaluation is inefficient due to duplicate work: ...
4
votes
1answer
138 views

Mathematical equivalent of reduce()?

filter() in functional programming can be thought of as being analogous to an equation that filters the range of the variable. map() can be through of as a function mapping domain to codomain. ...
4
votes
0answers
47 views

Inferring ranking functions in a general code graph with partial information

Let me define the notion of call graph: A program consists on a set of functions $f,g,h,\ldots$ where each function $n$ is as a mapping $n: D^l \to D^m$. Here $D$ is the datatype representing ...
4
votes
0answers
254 views

Why most purely functional red-black trees are left-leaning?

Is there any particular reason for picking a left-leaning red-black tree over a regular red-black tree when trying to do a purely functional implementation? I've not researched very deeply into this ...
4
votes
0answers
114 views

Is there any research to indicate programmers are/are not moving to a hybrid of functional and object-oriented?

I am converting the OCaml Format module which does I/O and maintains state in a record with mutable values. As such it is a good candidate for me to convert to pure F#, pure C# and a hybrid. Since ...
3
votes
3answers
175 views

Is it possible to make a language that can build upon itself perfectly?

First of all, note that I'll have to explain my thoughts in a layman's terms. There are so many high-level programming languages out there that compete with each other. This means we have to build ...
3
votes
2answers
72 views

Can we define a program by means of a walk of a graph induced by the category of types?

After reading about Category Theory at https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/ I was wondering whether we can represent any program by means of a walk of a ...
3
votes
5answers
531 views

functional programming in terms of Set

I'm writing some notes about functional programming, so I'd want to describe some features of the category theory. I visited wiki page about Category of Set, and I found this: "The epimorphisms in ...
3
votes
2answers
101 views

When is cumulative type universes useful?

AFAIK, a hierarchy of type universe(Type^0: Type^1: Type^2: ...) was introduced to avoid inconsistency caused by Type: Type. ...
3
votes
1answer
436 views

Does a Haskell program count as an inductive proof?

Is the following statement from [1] true? "Since recursion is the main computational technique, a terminating pure Haskell program counts as an inductive proof of a theorem." My intuition is that ...
3
votes
2answers
858 views

What type of formal notation is being used here to represent functional algorithms?

Interested in learning more about algorithm design in functional programming, I picked up Andrew Bird's Pearls of Functional Algorithm Design. I have experience with a number of programming languages,...
3
votes
1answer
713 views

Recursive definition of Matrix

Like Linked-list for Array, is there a recursive counter-part for Matrix? Is there a persistent data structure which can be used in place of Matrix in pure functional language like Haskell?
3
votes
1answer
594 views

Intuition behind F-algebra

I looked at here for getting an intuition about F-algebra, but I am still left with some questions. Suppose I have a group signature as $\Sigma= (* : X \times X \rightarrow X, \thicksim: X \...
3
votes
1answer
51 views

What are different ways to provide a semantics to a language?

Suppose you have 1. a grammar for terms of a language; 2. type-assignment rules, 3. a set of reduction rules. You want to prove that your language is adequate for mathematical reasoning. If I ...
3
votes
1answer
146 views

Does the closure of a function include the actual parameter passed to the function?

A closure of a function includes the environment when calling the function. Does the environment included in a closure of a function include the actual parameters for the function? If I am correct, ...
3
votes
1answer
171 views

explaining $\lambda$-calculus/functional programming to someone used to Turing machines/procedural programming?

I have the following background: I have experience with object-oriented programming languages I find Turing machines and the concept of a "procedure" very intuitive. Yet I'm interested to ...
3
votes
1answer
60 views

How to explain/understand brackets of applicative functor [[f u1… un]]?

I am reading article about Applicative Abstract Categorial Grammars http://okmij.org/ftp/gengo/applicative-symantics/AACG.pdf and this article uses brackets [[...]] for action on terms inside ...
3
votes
2answers
44 views

Is there a formal term for functions that have static state across executions?

Two examples, one in PHP: function adder($i){ static $a = 0; $a += $i; return $a; } A similar effect can be achieved with closures in javascript: ...
3
votes
1answer
75 views

Guessing the structure of a finger tree from the number of elements

I'm writing a data structure library, and I want to write an efficient algorithm for adding many elements to a finger tree (from an iterable sequence). I'm going to do this by constructing a finger ...
3
votes
1answer
37 views

“Immediate” method of translating arbitrary mutable program to equivalent unmutable program?

Consider the following program in "mutable style": x=1 x=f(x); x=f(x); We can rewrite this in "immutable style" without changing the higher-level structure of ...
3
votes
2answers
94 views

When are you supposed to eta-reduce?

Wikipedia lists the following algorithm for normalizing a lambda calculus term $t$: If $t$ is not in head normal form, beta reduce the beta redex in the head position to get $t'$. Then normalize $t'$ ...
3
votes
1answer
175 views

What type of function is main()?

As the functions are of 2 type:1.Pre-defined/library functions,2.User defined functions. What type of function is main() function? This doubt comes in my mind while writing a program we define the ...
3
votes
1answer
350 views

ML - Type Interface

From my recitation class - Can you please explain why does operator $"+"$ signature is $ int \rightarrow (int \rightarrow int)$ ? How does this graph is build ? And what is mean $t=u \...
3
votes
1answer
316 views

Why does higher-order abstract syntax need an inverse to define catamorphisms?

In the introduction to the colorfully-named Boxes Go Bananas: Encoding Higher-Order Abstract Syntax with Parametric Polymorphism, Washburn and Weirich describe a problem in traditional formulations of ...
3
votes
1answer
50 views

Intuition for “run” function of monads

I'm learning about monads, I understood why they are useful, I understood in general what bind, join, return do. I also looked at basic usage examples for the basic reader / writer / state / list / ...
3
votes
1answer
87 views

What is a proof of normalization of Morte?

It is said that any term on the calculus of construction halts. I am studying it through Morte, which is a bare bone implementation of the coc available on github. Is there any simple proof of ...
3
votes
1answer
56 views

Lower complexity bounds without mutation

Lower complexity bounds tend to be a very hard problem in general. Despite this, I was wondering if there are any theoretical results that relate lower complexity bounds for some class of problems in ...
3
votes
1answer
44 views

What additional expressivity does polyvariance give in pushdown CFA?

I'm reading through Pushdown Control-Flow Analysis of Higher-Order Programs, which presents a synthesis of the Abstracting Abstract Machines technique and pushdown automata to get static analysis ...
3
votes
0answers
96 views

Alternative to a CALL as a composition?

I've seen a numerous interesting abstract machines (i.e. CESK) and evaluators (diverse meta-circular S-expression evaluators, i.e. vau, COLA) and other models (concatenative, SK/Lambda calculus) which ...
3
votes
0answers
157 views

Is there any programming system that enables reversible computations?

Better explained with examples, I need a programming system with the following characteristics: ...
2
votes
4answers
148 views

How does one formally show that two lambda functions are $\alpha$ equivalent?

I was going through the following slides and I wanted to show the following: $$ \lambda x. x \equiv_{\alpha} \lambda y . y$$ formally. They define a an $\alpha$-conversion on page 15 as follows: $$ ...
2
votes
2answers
88 views

How does one show $(\lambda x . (\lambda y.x))yx \equiv_{\beta} y$ in lambda calculus?

I wanted to show: $$ (\lambda x . (\lambda y.x))yx \equiv_{\beta} y $$ the definition of beta equivalence is on page 17 of these notes. I did a few attempts but got different things like $x$. I ...
2
votes
1answer
1k views

Reducing lambda expression to normal form

Can someone explain the steps to reduce $$ (\lambda n. \lambda m. \lambda f. \lambda x.\ n\ (m\ f)\ x)\ (\lambda f. \lambda x.\ f\ (f\ x))\ (\lambda f. \lambda x.\ f\ x) $$ to $\lambda y. \lambda z.\...
2
votes
2answers
112 views

Lambda Calculus Prove Equality Excessive (Haskell-oriented)

I'm on a lambda calculus with parametric polymorphism a la Hindley-Milner Haskell-oriented course and I'm currently facing this exercise which I got stuck on. Prove that $(\forall m\downarrow, n\...