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

-1
votes
0answers
5 views

Comparing Two Lists in SML using Fold/Map? [migrated]

Say I have two lists, [1,2,3] and [9,2,3]. Say I'm given a third element, 2. If I want to find out if two is in both lists, but I can only use foldl/foldr/map to do so (no let environments or custom ...
0
votes
1answer
48 views
5
votes
0answers
30 views

Can we simulate any dependent datatype with `Eq`?

Consider the canonical homogeneous equality type: Eq : (A : Set) -> A -> A -> Set, with constructor ...
3
votes
0answers
31 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 ...
8
votes
1answer
50 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
179 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
79 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
21 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
68 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
50 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
21 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 ...
19
votes
3answers
118 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
31 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 ...
5
votes
2answers
260 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 types systems, such as SML or Elm). If I have a type signature ...
0
votes
1answer
24 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
60 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 ...
5
votes
1answer
142 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
32 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. ...
7
votes
0answers
127 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
21 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
57 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
78 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
134 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
22 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
53 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
90 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
144 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: ...
7
votes
1answer
106 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
21 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
101 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
126 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
33 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
74 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 ...
0
votes
0answers
18 views

Proxy for lazy evaluation?

Can lazy evaluation be substituted in an eagerly evaluated language by the following setup?... Higher-order functions. Generalized left associativity. Infinite structures like ...
2
votes
1answer
30 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
123 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
58 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
515 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
51 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
25 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
90 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
85 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 ...
3
votes
3answers
652 views

Does immutability in functional programming really exist?

Although I work as a programmer in my daily life and use all the trendy languages (Python, Java, C, etc) I still have no clear view of what functional programming is. From what I've read, one property ...
4
votes
1answer
67 views

Using SMT solvers to generate random solutions to given predicate

I am interested in generating random solutions to predicates. I only need SMT for integers with the following predicates/functions <, >, <=, >=, ==, !=, +, * The algorithm I want should produce ...
1
vote
1answer
51 views

Substitution-based Operational Semantics of algebraic datatypes

Assume, I want to define the operational semantics for some subset of ML. ...
2
votes
2answers
69 views

Second order function formalization

I need to work on a optimizer for a language whose operator are second order functions. They are the well known ones filter, map, reduce, fold, foreach etc. etc. I need to formalize as much as ...
1
vote
2answers
75 views

Is it possible to write an HTML compiler with no mutable state?

That's probably a vague question but allow me to try and give an example: My compiler does transformations on HTML (from HTML to HTML). It scans a flattened DOM tree, and relies on lookbehinds (on ...
-2
votes
1answer
115 views

Logic and Functional programming [closed]

I have a subject Introduction to logic and functional programming but the course is not provided in detail. This is the provided course. Introduction to declarative programming paradigms. The ...
1
vote
0answers
54 views

How to get from factorial to a y-combinator?

In one of his conference talks Jim Weirich derives the applicative form of the y-combinator by refactoring a partial definition of factorial. The starting point in his talk is different than what ...