Skip to main content

Questions tagged [functional-programming]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
3 votes
3 answers
106 views

Can parametricity be applied to show a property of function values?

Say I have the following dictionary of abstract operations, written in Haskell for relatively concise notation: ...
Sebastian Graf's user avatar
3 votes
2 answers
124 views

How to prove that $\exists A. ~ A \times (A\to F~ A)$ encodes the greatest fixpoint of $F$?

Following Wadler's paper "Recursive types for free" and having spent some months on reconstructing the proof that $\exists A. ~ A \times (A\to F~ A)$ is the terminal $F$-coalgebra, I am ...
winitzki's user avatar
  • 542
4 votes
0 answers
84 views

Is the encoding of existential types in System F adequate?

This is somewhat related to How to encode a function from an existential type Existential types can be encoded in System F. If $P$ is any type constructor, not necessarily covariant, then the ...
winitzki's user avatar
  • 542
2 votes
1 answer
108 views

A monad law about bind and function composition

This law about bind and function composition type checks: bind m (f o g) = f (bind m g) but it is not clear whether it is true and how can it be proved. How could ...
Gergely's user avatar
  • 123
3 votes
3 answers
201 views

Can we use relational parametricity to simplify the type $\forall a. ( (a \to a) \to a ) \to a$?

This question is about using relational parametricity to resolve practical questions in pure functional programming in System F. Consider the following type of polymorphic functions: $$T = \forall a. ...
winitzki's user avatar
  • 542
4 votes
1 answer
164 views

Is there a high level (functional) language compiling to Mixed Integer Linear Programming problems?

Many different kinds of optimization problems can be expressed as Mixed Integer Linear Programming (MILP). The translation is usually very direct, and one has to encode invariants as constraints in a ...
Turion's user avatar
  • 646
1 vote
0 answers
68 views

Primitive recursion relative to a logical system

In various places I have read that the normally considered non-primitive recursive Ackermann function is primitive recursive in higher-order logic. It's claimed to be due to "Reynolds, 1985",...
Ilk's user avatar
  • 920
0 votes
0 answers
85 views

How does laziness help functional data structure?

Functional data structures, or immutable data structures, are often achieved by copying old data to new data upon operation. Naively, it looks much less efficient than their imperical counterpart. ...
Student's user avatar
  • 127
4 votes
2 answers
321 views

Composition with recursion in functions between types

I always understood functions in functional programming to be modeled by morphisms in the category of types, where any powerful function you write in your code is a morphism that is the composition of ...
Ryan's user avatar
  • 43
2 votes
2 answers
183 views

Can we use relational parametricity to simplify the type $\forall a.\,((a\to r)\to a)\to a$ and similar types?

This question is similar to Can we use relational parametricity to simplify the type $\forall a. ( (a \to r) \to r ) \to (a \to r) \to r$? but looks more complicated. It is about using relational ...
winitzki's user avatar
  • 542
3 votes
1 answer
152 views

Can we use relational parametricity to simplify the type $\forall a. ( (a \to r) \to r ) \to (a \to r) \to r$?

This question is about using relational parametricity to resolve practical questions in pure functional programming in System F. Consider the following types of polymorphic functions: $$ \forall a.\, (...
winitzki's user avatar
  • 542
0 votes
1 answer
369 views

What is a "Covering Function"?

In Idris2, I will sometimes get an error telling me that a function "is not covering", which is apparently distinct from it not being total (and I do understand what a total function is). I ...
MCLooyverse's user avatar
2 votes
1 answer
192 views

Intuitive way to handle variable binding

Suppose we have an algebraic datatype parameterised by a type variable name, e.g. ...
A confused dove's user avatar
3 votes
1 answer
151 views

Encapsulation of OOP and referential transparency of functional programming

I would like to understand more about the 'orthogonality' of OOP and functional programming. What makes me confused is the 'encapsulation' of OOP and 'referential transparency of functional ...
Chanwoo Ahn's user avatar
-1 votes
1 answer
92 views

Is function composition associative in non-pure programming languages?

We know that function composition is associative in theoretical programming languages such as STλC, and pure functional programming languages such as Haskell. Is the same true for languages where ...
Michele De Pascalis's user avatar
4 votes
3 answers
378 views

Kleisli-like category for applicatives?

I am wondering if there is a good way to complete the following analogy: monad : Kleisli category :: applicative functor : ?? That is, a given monad T on a ...
Julian G.'s user avatar
2 votes
0 answers
73 views

$[[ \text{fn} \ x => [x]^1]^2 [ \text{fn} \ y => [y]^3]^4]^5$ calls the identity function $\text{fn} \ x => x$ on the argument $\text{fn} \ y => y$?

This is question is related to this past question. I am currently studying the textbook Principles of Program Analysis by Flemming Nielson, Hanne R. Nielson, and Chris Hankin. Chapter 1.4 Constraint ...
The Pointer's user avatar
2 votes
1 answer
152 views

Phonology and lambda calculus

I wonder whether there is any relationship between lambda calculus and phonology (study of phonemes). Specifically, how one would use the concepts of lambda calculus (typed or untyped) in the study of ...
Jacob Hjortmann's user avatar
1 vote
0 answers
91 views

What is the time complexity of substitution algorithms(normalization by evaluation, explicit subtitution)?

I'm studying the substitution algorithms of lambda calculus. I think now I understand how they work, but I couldn't find any materials about their time complexity yet. This is what I've thought about ...
user42215's user avatar
  • 119
4 votes
1 answer
495 views

Areas of research and open problems in functional programming [closed]

What are the major areas of functional programming that require more research and development? For example, I know a lot of people are asking for dependent types in Haskell, and someone at my uni is ...
otah007's user avatar
  • 141
1 vote
0 answers
289 views

How do computers check if two functions are the same?

To prove that two given functions are the same involves proving infinitely many statements. I wonder how to implement so that a computer can check such a statement? An easy example is the following: ...
Student's user avatar
  • 127
6 votes
1 answer
323 views

Fixed set of type constructors to simulate all intensional inductive families?

I'm wondering, are there small dependent calculi that can simulate a language with inductive families (that is, has a type isomorphic to each inductive family, at least as powerful of induction ...
Joey Eremondi's user avatar
6 votes
1 answer
234 views

Structural equality of Pi Types with heterogeneous equality?

I'm trying to implement a proof of the following type: ...
Joey Eremondi's user avatar
8 votes
2 answers
875 views

What category are Tagless Final Algebras final In?

The Haskell and Scala community have been very enamored recently with what they call tagless final 'pattern' of programming. These are referenced as dual to initial free algebras, so I was wondering ...
Henry Story's user avatar
9 votes
3 answers
513 views

Can Non-termination be considered an algebraic effect?

Non-termination is sometimes considered an effect. I have been reading about algebraic effect systems (What is algebraic about algebraic effects and handlers?), and I suspect non-termination (like ...
user833970's user avatar
10 votes
2 answers
1k views

What logic correponds via Curry-Howard to a Monad?

According to Moggi's 1991 paper "Notions of computation and monads" one can represent monadic equational logic with the well known monad $(T, \eta, \mu)$ with T an functor and the two natural ...
Henry Story's user avatar
3 votes
0 answers
417 views

Is it possible to check equality of equi-recursive types, or recursive λ-terms?

Can we determine if two λ-terms are equal? Given two lambda terms, let's say they are equal if their (possibly infinite) Bohm trees are. Under this definition, for example, ...
MaiaVictor's user avatar
  • 3,177
7 votes
3 answers
497 views

When a type is a value?

In functional programming and in the theoretical setting of the $\lambda$-calculus it is standard to consider a lambda abstraction $\lambda x.M$ as a value. In my understanding, the intuitive reason ...
Domenico Ruoppolo's user avatar
6 votes
0 answers
170 views

Immutable Space Model

I have heard it said that time is more precious than space because we can reuse space but not time. What if we treat space with this much reverence? What is generally known about models of ...
Tyson Williams's user avatar
2 votes
0 answers
128 views

A categorized (?) list of functional pearls in JFP and ICFP

Is there a list of (categorized preferred) functional pearls ever published in ICFP and JFP? I could go to the ICFP proceedings and JFP issues and find all of them, but this would be time-consuming. ...
xrq's user avatar
  • 1,185
5 votes
1 answer
138 views

Topology/Space of Recursive Algebraic Datatypes

I have a recursive algebraic datatype. I (somewhat arbitrarily) defined one function to compute distance between instances, and am trying to define a function to approximate a "vector" between ...
lightning's user avatar
  • 433
3 votes
1 answer
140 views

Stream fusion in total functional language

As I understand, stream fusion consists in converting operations on lists to operations on streams (colists), optimize redundant codata to data and back conversions, fuse operations on streams, and ...
user3368561's user avatar
12 votes
1 answer
350 views

What makes a language (and its type-system) capable of proving theorems about its own terms?

I've recently attempted to implement Aaron's Cedille-Core, a minimalist programming language capable of proving mathematical theorems about its own terms. I've also proven induction for λ-encoded ...
MaiaVictor's user avatar
  • 3,177
6 votes
1 answer
221 views

Can all structurally recursive functions be written without explicit recursion using a catamorphism/fold?

In particular, I am thinking of a function which involves conditionals changing the recursive behavior and multiple F-algebras. ...
lightning's user avatar
  • 433
4 votes
0 answers
523 views

Is it possible to derive induction by extending CoC with recursion?

Suppose we extended the CoC with primitive recursion; that is, we added a term µ x . t such that equality allowed unrolling recursive terms: ...
MaiaVictor's user avatar
  • 3,177
8 votes
1 answer
179 views

Type for "ways values can be different"

I am looking for a concept in type theory that I am sure has probably been explored, but do not know the name behind. Let's consider a ML-like language with product and sum types and a Hindley-Milner ...
Étienne Millon's user avatar
0 votes
0 answers
297 views

Can $f^{2^N}(x)$ be computed in polynomial time when $f$ is linear?

Linear functions: definition Let's define a linear function as one expressible as an untyped λ-calculus term with the added restriction that no lambda argument can be used twice. Linear functions: ...
MaiaVictor's user avatar
  • 3,177
1 vote
0 answers
49 views

Is it possible to use arbitrary fixpoint values on EAL without losing strong normalization?

From this question, the answerer states EAL-based languages can use arbitrary fixpoint types without losing strong normalization, because their normalization (and complexity) properties comes from ...
MaiaVictor's user avatar
  • 3,177
6 votes
1 answer
123 views

Can you assign a type to any term of the λEA-calculus?

The untyped language of System-F and similar is the λ-calculus. That language has terms that can't be typed on System-F, λx.(x x) λx.(x x) being the most obvious ...
MaiaVictor's user avatar
  • 3,177
2 votes
1 answer
752 views

Wouldn't the calculus of constructions with linear types be a simple functional core that is consistent and expressive?

I have recently asked if there is a simple functional core that is consistent and expressive. In another question, cody pointed out that this is an open problem to have a language that is: Consistent/...
MaiaVictor's user avatar
  • 3,177
14 votes
0 answers
436 views

Are there simple core languages which are consistent and expressive?

The Calculus of Constructions is a very simple core functional language with dependent types. Per curry-howard isomorphism, it could, potentially, be very useful for writing programs and proofs. It, ...
MaiaVictor's user avatar
  • 3,177
6 votes
1 answer
168 views

Programming language supporting infinitary rewriting of regular term graphs?

Do any practical programming languages support term graph rewriting of infinite but regular terms? For example the toy language CoCaml [1] supports computations on infinite regular streams. Coq ...
fritzo's user avatar
  • 265
5 votes
4 answers
864 views

Purely(ish) functional data structure with fast append and forward iteration

I find I have need for a data structure with a specific set of requirements: It represents an immutable sequence of values (fixed sized integers if this matters) Appending a new value to the end (and ...
DRMacIver's user avatar
  • 444
15 votes
3 answers
581 views

(How) Could we discover/analyze NP problems in the absence of the Turing model of computation?

From a purely abstract math/computational reasoning point of view, (how) could one even discover or reason about problems like 3-SAT, Subset Sum, Traveling Salesman etc.,? Would we be even able to ...
PhD's user avatar
  • 5,335
15 votes
1 answer
3k views

Why do functional programming languages require garbage collection?

What's stopping ghc from translating Haskell into a concatenative programming language such as combinatory logic and then simply using stack allocation for everything? According to Wikipedia, the ...
Nicholas Grasevski's user avatar
2 votes
0 answers
177 views

Is there is an intuitive explanation why call-by-name PCF is less expressive than both call-by-value PCF and lazy PCF?

J.C. Mitchell cites in his "Expressive power of programming languages" the result in Riecke's "Fully abstract translations between functional languages" about the call-by-value, call-by-name and lazy ...
Akram El-Korashy's user avatar
1 vote
1 answer
155 views

Observational Equivalence of open terms in PCF

The notion of observational equivalence is rather intuitive, but formally I'm having some doubts in the particular case of open terms. Lets consider the simple case where the terms ...
Adribar's user avatar
  • 31
-3 votes
1 answer
533 views

Can we say that Church encoding is a form of Gödelization?

We see here the following statement about Godelization: Gödel numbering in computer science means more or less "source code" and "data in binary format", so I hope the ...
hawkeye's user avatar
  • 2,581
1 vote
0 answers
79 views

Best Asymptotic Complexity for Persistent Union Find

In this paper https://www.lri.fr/~filliatr/ftp/publis/puf-wml07.pdf, they claim to have a practically fast persistent union-find data structure for most use-cases, but it's still not polylogarithmic ...
dspyz's user avatar
  • 916
6 votes
1 answer
363 views

What type system fits the subclass of λ-terms that can be reduced optimally?

There is a subset of λ-calculus terms that can be reduced by Lamping's Abstract Algorithm without using the Oracle. That is an interesting subset, because only for those terms it is proven that ...
MaiaVictor's user avatar
  • 3,177