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
8
votes
1answer
163 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 ...
8
votes
1answer
505 views

Simply Typed Combinatory Logic?

As there is an untyped lambda calculus, and a simply-typed lambda calculus (as described, for example, in Benjamin Pierce's book Types and Programming Languages), is there a simply-typed combinatory ...
8
votes
2answers
171 views

What is the state of the art in encapsulated search in functional logic programming?

I am particularly interested in solutions to the problem that encapsulated search can depend on the order of evaluation. According to [1], encapsulated search in PAKCS depends on the order of ...
7
votes
2answers
403 views

Total functional programming language without an static type checker

All papers with the subject of total functional programming make use of some kind of static type checking to ensure totality. This make sense considering hoy easily is to make a language Turing-...
7
votes
1answer
129 views

Can literals in functional languages be thought of as functions from the empty type?

A while ago, I think on Stack Overflow, I saw someone say that Haskell literals can be thought of as functions that don't operate on anything. This makes sense to me but I remember someone else ...
7
votes
2answers
678 views

Higher-ranked polymorphism without explicit application or subtyping?

So, I'm familiar with two main strategies of having higher-ranked polymorphism in a language: System-F style polymorphism, where functions are explicitly typed, and instantiation happens explicitly ...
7
votes
1answer
604 views

How is IO a monad?

I am learning the Haskell programming language. From what I am reading, Input/Ouput (IO) raises challenges for Haskell's purity, since by definition we are interacting with the outside world. From ...
7
votes
1answer
314 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 ...
7
votes
2answers
641 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 ...
7
votes
1answer
1k 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: ...
7
votes
1answer
207 views

Y combinator, function composition

I am trying to understand Y combinators. Could you please explain why the following are equivalent (Y (f ∘ g)) (f (Y (g ∘ f))) (Y is a fixed point combination)...
7
votes
2answers
178 views

Why Church-encoded types aren't sufficient to express inductive proofs?

I've heard some claims that the calculus of constructions without inductive types isn't powerful enough to express proofs by induction. Is that correct? If so, why isn't the Church-encoding sufficient ...
7
votes
0answers
36 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 ...
6
votes
2answers
2k views

Difference between multimethods and overloading

Context I've been programming in java for a few years now. And atm i'm learning something totally different: Clojure. There the expression problem can be solved by using multimethods whereas in java ...
6
votes
1answer
356 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 ...
6
votes
2answers
296 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 ...
6
votes
1answer
655 views

Is Equational Reasoning an application of Referential Transparency?

In various discussions of the merits of functional programming, the phrase referential transparency or equational reasoning is often listed. My question is - are these roughly the same thing? (One ...
6
votes
1answer
378 views

Why are the laws of an applicative functor defined the way they are?

Let's recall the definition of an applicative functor. Throughout this question, I write $x: T$ to denote that the value $x$ has type $T$. Definition: An applicative functor consists of a type ...
6
votes
2answers
89 views

Representing partialled/curried functions in postfix notation?

I'm working on a small query language in JSON. A query consists of a JSON array of JSON elements, such as strings, numbers, booleans, etc. Strings starting with a ...
6
votes
1answer
246 views

How is the definition of monads in category theory equivalent to the definition in functional programming?

In Haskell, Monad is a class of type constructors which act on types that have the following functions implemented: ...
6
votes
1answer
215 views

Safe way to explicitly define new types instead of using Algebraic data types for my functional language

Question: As I'm working on a Hindley-Milner typed lambda calculus, in order to make it usable I need to add some types such as list and pairs. The way I currently do it is, I have an ...
6
votes
2answers
204 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: ...
6
votes
1answer
406 views

Lazy concatenative functional language

Can the idea of concatenative programming languages be extended to call-by-need evaluation strategy? I see some problems that I will explain with few examples. I will use a prefix instead of a ...
6
votes
2answers
221 views

Reference request: Monads, continuations, and other functional CS concepts

I've been using Clojure for about 18 months. Recently, I've come across terms such as Monads, Continuations, et al which I'd like to learn about. I could visit Wikipedia and read about these two ...
6
votes
1answer
99 views

Can we express the program to find last element of a list as a catamorphism?

So I've got a bit of category theory under my belt, and I am reading a few papers about calculating functional programs. I've expressed programs like summing a list as a catamorphism, and I've fused ...
6
votes
1answer
173 views

Is it possible to prevent arithmetic errors with a dependent type system?

In a functional programming language I have functions like $$f\colon Int \times Int \times \cdots \times Int \to Int$$ which do some computation. However for certain arguments $(x_0, \dots, x_n)$ the ...
6
votes
2answers
1k 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 ...
6
votes
0answers
58 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. ...
6
votes
0answers
96 views

Bounded existential polymorphism

In his "Types and Programming Languages", Pierce, at the very end, presents the most powerful system in the book: $F^{\omega}_{<:}$. He, however, does not explain how bounded existential ...
6
votes
0answers
82 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 ...
5
votes
3answers
2k views

Are the words “expression” and “term” interchangeable in programming language theory?

When describing the syntax of a given programming language the words "expression" and "term" are often used to seemingly describe the same things. Are these words interchangeable in the context of ...
5
votes
3answers
86 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) ...
5
votes
4answers
109 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 ...
5
votes
2answers
271 views

Is there a point to an all-encompassing programming language? [duplicate]

There are many programming languages in use throughout the world today, including languages that specialize in database manipulation, functionality, object-orientation, concurrency, etc. Would there ...
5
votes
3answers
122 views

How exactly do we define parametric polymorphism?

My naive distinction between parametric polymorphism and ad-hoc polymorphism, is that: In parametric polymorphism, the type is given as a variable: (pseudocode) Function f: <.Type T> T $\to$...
5
votes
1answer
341 views

Why is Church-Rosser so important for basing programming languages on lamdba-calculus?

So, I know Church-Rosser has 2 thesis: CR1: If $ E_1 \leftrightarrow E_2 $, then there exists an Expression E so $ E_1 \rightarrow E $ and $ E_2 \rightarrow E $ CR2: If $ E \rightarrow N $ (with N ...
5
votes
2answers
430 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
1answer
149 views

What progress has been made on persistent catenable deques in the last decade?

I'm interested in persistent catenable deques: deques that can be concatenated. Kaplan and Tarjan came up with the first such data structure in 1995; Okasaki came up with a simpler, amortized version ...
5
votes
1answer
1k views

call by value: what is a value?

In the 'call by value' evaluation of lambda-calculus, I am bit confused with 'value'. On page 57 of the book Types and Programming languages, it is said: The definition of call by value, in which ...
5
votes
3answers
2k 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 ...
5
votes
1answer
395 views

Non-termination of types in Martin-Löf's Type:Type?

In the pre-history of dependent type theory, Per Martin Löf introduced a calculus that is in some sense the simplest dependent type theory and the most general form of impredicative polymorphism. It ...
5
votes
2answers
436 views

Why don't imperative languages like C or Go support Haskell-like parametric polymorphism?

Why don't imperative languages support parametric polymorphism as powerful as whats in Haskell and OCaml? More specifically if I call a function foo(x) that ...
5
votes
2answers
264 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 ...
5
votes
1answer
292 views

How to write a coterminating, effectful program?

[Using Idris for code examples and terminology, but the question is not about Idris per se] In a post titled A Neighborhood of Infinity, @sigfpe argues that "the kind of open-ended loop we see in ...
5
votes
1answer
295 views

About the relationship between non-termination and inconsistency?

I've been trying to get into Agda and I noticed that it doesn't have recursion, which implies that it isn't Turing-Complete. From what I could understand, if Agda had recursion, it would make itself ...
5
votes
1answer
151 views

What are some possible “functional” memory structures?

With my thin knowledge on embedded systems, compilers, and computer architectures, I know that the basics of computer memory(physical) are sort of like an array, with addressing which work like ...
5
votes
1answer
166 views

Best way to translate while loops to functions for software verification

I have a verification engine where while loops are translated into functional code, like this: ...
5
votes
1answer
112 views

strong reduction of $\lambda$-terms, useful?

As we know many programming languages and systems don't implement the strong reduction of $\lambda$-terms, instead they do weak reduction (no reduction under abstraction). I recently experimented ...
5
votes
1answer
485 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 ...
5
votes
1answer
75 views

Is dependency analysis required in order to type a program?

I have seen stated in various places that in order to allow an "increase in polymorphism," functional dependency analysis should be performed, and type inference should be used for every declaration ...