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

learn more… | top users | synonyms

0
votes
1answer
28 views

Is function application actually a memory manipulation algorithm?

I thought about how in lambda calculus (and many implementations of functional programming languages) function (lambda) application and lambda itself, as a construct, are "primitive things", usually ...
0
votes
1answer
54 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?
1
vote
0answers
41 views

Tricks, Tips and Nontrivial Insights with Higher-Order Functions

Many years ago I briefly skimmed a physical book (or perhaps a preprint?) on programming in Racket that included lots of really unique uses of map and ...
5
votes
1answer
57 views

How to find time complexity for functions in lazy functional languages?

So far, I have looked around the internet for information how to find the time complexity for functions in lazy functional languages, but most of the resources on time complexity focus on strict ...
7
votes
1answer
66 views

Why is `map insertionsort` not to equal to`map mergesort`?

In the type theory podcast ep. 3, Dan Licata claims that the fact that for every input, insertionsort and mergesort give the same result does not imply that the result would be equal when used as ...
0
votes
0answers
24 views

How would one prove that the following scheme definition is an ordered stream of integers

How would one prove that the following scheme definition is an ordered stream of integers (define integers (cons-stream 1 (add-streams ones integers)))
4
votes
3answers
51 views

Is Applicative-order and Normal-order evaluation model's definition contradictory as per sicp text book?

As per this explaination, it defines applicative and normal order evaluation in one form saying: This alternative "fully expand and then reduce" evaluation method is known as normal-order ...
3
votes
2answers
51 views

Functional programming with branches that have no order?

I was wondering if there is any programming style in which the outcome does not depend on the order of statements or groups of statements such as guards. Vaguely, I imagine this would leave room for ...
1
vote
1answer
59 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 ...
0
votes
1answer
58 views
5
votes
0answers
39 views

Can we simulate any dependent datatype with `Eq`?

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

Flaw with Cross Entropy Error in Neural Networks

I've recently been working on creating a neural network to classify handwritten digits. I implemented 1-of-N encoding such that there are the same number of output nodes as possible digits (The ...
10
votes
1answer
72 views

No Naive Set Theoretic Models of Polymorphic Lambda Calculus?

In Philip Wadler's paper on Theorems for Free he states in Section 2 on Parametricity that there are no naive set-theoretic models of polymorphic lambda calculus In the naive set-theoretic model ...
8
votes
2answers
191 views

Proving a sorting operation in type system

I want to know how far a type system in a programming language can be beneficial. For example, I know that in a dependently typed programming language, we can create a Vector class incorporating size ...
7
votes
1answer
100 views

Can we do everything in imperative languages with a functional language if it does not allow for a 'state'?

I was reading Structure and Interpretation of Computer Programs (SICP), MIT. What I have understood is that in pure functional programming language, there is no such thing as a local state. SICP, pg ...
0
votes
1answer
24 views

The symbolic differentiation of univariate expressions

I was reading "Doug McIlroy: McCarthy Presents Lisp" and the phrase "symbolic differentiation of univariate expressions" triggered a faint memory of a demonstration of differentiation done in haskell ...
4
votes
1answer
78 views

Do Self Types make the Calculus of Inductive Constructions obsolete?

Self Types are an extension of the Calculus of Constructions [1] that allow the language to express algebraic datatypes encoded through the Scott Encoding. The Scott Encoding provides one the ability ...
2
votes
1answer
69 views

Why do we distinguish between term abstraction and type abstraction in System F?

In System F, we distinguish between types and terms. Types are defined by the following BNF: \begin{align} A, B ::=&~\alpha && \text{(type variable)} \\ &|~A \rightarrow B ...
1
vote
0answers
22 views

What is a proof of normalization of Motte?

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 ...
22
votes
3answers
188 views

What is a brief but complete explanation of a pure/dependent type system?

If something is simple, then it should be completely explainable with a few words. This can be done for the λ-calculus: The λ-calculus is a syntactical grammar (basically, a structure) with a ...
4
votes
2answers
35 views

What terms type systems exclude?

I understand type systems like the simply typed lambda calculus, system F and the calculus of constructions include a different subset of all lambda terms. But what, precisely, are the terms each of ...
6
votes
2answers
340 views

In the Curry-Howard isomorphism as applied to Hindley-Milner types, what proposition corresponds to a -> [a]?

(Using Haskell syntax, since the question is inspired by Haskell, but it applies to general Hindley-Milner polymorphic type systems, such as SML or Elm). If I have a type signature ...
0
votes
1answer
26 views

How can a device decipher spoken English words?

I want to know how it can process spoken English words and Pull out a matching response? Is it a chip or a installed software? Does it take up a lot of space? Thanks.
5
votes
1answer
72 views

What is the Curry-Howard analogue for linear logics?

As defined by Wikipedia, (The Curry-Howard correspondence) is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the ...
6
votes
1answer
171 views

Can a functional language be homoiconic?

According to the wikipedia page on homoiconicity: In a homoiconic language the primary representation of programs is also a data structure in a primitive type of the language itself. I was ...
5
votes
0answers
35 views

Is it possible to reduce functional equations to SAT?

The problem of finding a solution for functional equations can be defined as: Let A0, A1, A2... An, B0, B1, B2... Bn, X be terms of the lambda calculus, all terms known, except for X, unknown. ...
8
votes
0answers
150 views

Are CPU architectures biased towards procedural runtimes?

Are there any changes that could be made to CPUs to make them perform better for concurrent runtimes like Rust? For instance, are there changes to branch prediction implementations or cache sizes ...
0
votes
1answer
25 views

Proving equality between foldl recursive and iterative fold

Hi I have two definitions of fold. I will call them foldl which is recursive and fold$_{itr}$ which is iterative. I am looking for an algebraic proof that the two definitions are equal ideally ...
0
votes
2answers
62 views

Expressing iterative version of fold in terms of recursive version

1st Definition. Recursive definition of fold fold$_{recur}$ (c,h) nil = c fold$_{recur}$ (c,h) (cons(a, x)) = h(a, fold$_{recur}$ (c,h) x) 2nd definition of fold. Iterative definition fold$_{itr}$ ...
1
vote
1answer
92 views

Can we prove mathematical induction statements in Lisp?

My previous question Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program? has a problem that it tries to cover too much ground. Here is a related question motivated by ...
3
votes
2answers
155 views

Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program?

Chapter 7 of The Haskell Road to Logic Math and Programming discusses induction and recursion. Haskell is strongly typed and we can define the natural numbers ...
3
votes
2answers
27 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: ...
4
votes
3answers
55 views

Is there any meaning behind the classification of “λ-terms” in classes such as “church number” and “church list”?

λ-calculus terms can be informally/intuitively categorized, such as: (λ f x . (f (f (f x))))) is a church natural (3) ...
0
votes
1answer
103 views

Why are functional programs considered slower than procedural counterparts asymptotically, if the opposite appears true?

I've read and been told way too many times that functional algorithms and data structures have an obligatory O(log(N)) slowdown in respect to their procedural ...
6
votes
2answers
151 views

Eliminate non-local references from closure

For a code similarity detection framework I need to eliminate references to non-local variables, for example having the following closure: ...
8
votes
1answer
116 views

Are combinatory logic terms always larger?

So there is an algorithm to convert lambda calculus terms to combinatory logic using SK combinators. It produces things that explode in size. I would like to know more about this explosion in size. I ...
6
votes
0answers
24 views

Is there any type system which can assign a type to any halting lambda calculus term? [duplicate]

Some lambda terms, such as the church number 3: (f x -> (f (f (f x)))), are easily typeable on the simply typed lambda calculus. Others, such as ...
2
votes
1answer
113 views

Do functional algorithms require more memory than imperative algorithms? [closed]

Let's suppose we are counting words in string. We split it so what we have is an array of strings. I'll use Python as an example. The imperative approach would as follows: ...
1
vote
1answer
151 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 ...
2
votes
2answers
39 views

Occurrences notation in “Compiling Pattern Matching to Good Decision Trees”

From Compiling Pattern Matching to Good Decision Trees (Luc Maranget, Proceedings of ML '08, pp. 35–46. ACM, 2008.) We also consider the usual occurrences. Occurrences are ...
1
vote
2answers
89 views

Curry Howard correspondence and Church-Turing thesis

Curry-Howard correspondence states the equivalence between logic/deduction and types/programs. The Church-Turing thesis states the equivalence of some models of computation. Specifically, all ...
3
votes
1answer
32 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 ...
2
votes
1answer
184 views

What is the difference between the Mogensen-Scott and the Boehm-Berarducci encoding for ADTs on the Lambda Calculus?

On the Lambda Calculus, there are several different ways to represent a list. For example, one can encode it as its right fold: ...
2
votes
1answer
56 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 ...
0
votes
1answer
61 views

Suggestions for Short Examples Contrasting Functional Programming Languages [closed]

A fellow student and I are writing a paper on functional programming for a programming languages course, part of which will be comparing and contrasting Lisp (Scheme), ML (SML), and Haskell. We'll be ...
1
vote
1answer
922 views

Difference between normal-order and applicative-order evaluation

The language I'm learning is Scheme and I'm working on an exercise that gives this: ...
1
vote
1answer
59 views

Definition of opposite category

From page 29 of The algebra of programming : For any category C the opposite category $C^{op}$ is defined to have the same objects and arrows as C, but the source and target operators are ...
0
votes
1answer
28 views

Something wrong with this definition of factorial with structural recursion? [closed]

In The Algebra of Programming page 5, the authors defined structural recursion foldn (c, h) over natural numbers: ...
3
votes
2answers
114 views

Formal Verification of Functional Programs

So I've been interested in learning more about formal verification, and I've seen a lot of interesting things like ACSL and JML which are based on the concept of Hoare triples. My question is, that ...
5
votes
4answers
90 views

Reviews of work in the field of partial evaluation (post 1993)

I'm looking for relatively new reviews of research work on partial evaluation. The most recent work I've found is "Tutorial notes on partial evaluation" by Charles Consel and Olivier Danvy (1993). The ...