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
1answer
115 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
496 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
76 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 ...
5
votes
0answers
48 views

Rules for consistency with mutual inductive families?

I'm trying to use a proof assistant to define a type and a relation that are mutually dependent on each other: ...
5
votes
0answers
80 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
60 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
3answers
955 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
514 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
88 views

Why is the second operation of a Monad called bind?

I understand how monadic computation works, I am just wondering where does the name come from. I cannot relate the thing that the bind operator actually does (i.e. ...
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
478 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
107 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
289 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
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
102 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 provide logic ...
4
votes
1answer
297 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
59 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
131 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
175 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
49 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
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
183 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
75 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
2answers
138 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
5answers
563 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
3answers
112 views

Can lists be defined in a special way so that they contain things of different type?

In https://www.seas.harvard.edu/courses/cs152/2019sp/lectures/lec18-monads.pdf it is written that A type $\tau$ list is the type of lists with elements of type $\tau$ Why must a list contain ...
3
votes
1answer
457 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
866 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
249 views

The meaning and relevance of the locution ''no terminating implementation'' in type theory

In the context of a discussion of Haskell https://stackoverflow.com/questions/62509788/the-intuition-behind-the-definition-of-the-co-reader-monad, I was told that There is no terminating ...
3
votes
1answer
741 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
649 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
102 views

Functional Programming and Category Theory

I'm a math Ph.D. having done research in Algebraic Geometry and Algebraic Topology in grad school for my thesis and I've studied a fair amount of category theory in the process (e.g. having worked ...
3
votes
1answer
53 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
150 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
181 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
65 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
2answers
93 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 sequences ...
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
2answers
302 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 ...
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
107 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
251 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
359 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
23 views

Pattern matching on function application

Suppose we have a function f :: a -> b and a function g :: b -> a such that f . g = id....
3
votes
1answer
55 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
91 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 ...

1 2
3
4 5
7