Questions tagged [functional-programming]
The functional-programming tag has no summary.
140 questions
-1
votes
0
answers
52
views
Specification languages for functional programming
I'm trying to understand the code of the functional language Factor. Many functions defined by mutual recursion, untangling a tangle of snakes, looking for tails. How can I clearly write down what I ...
0
votes
0
answers
79
views
What constitutes a functional program
I am trying to understand what is and isn't a 'program' in functional programming languages, in the way that all programs should return something (or, that they are values) and that programs are ...
- 109
5
votes
0
answers
193
views
How to use relational parametricity to simplify the type $\forall A.\,((A \to A)\to P)\to Q$
Question
Working in System F, consider the following type:
$$
T = \forall A.\,((A \to A)\to P)\to Q
$$
Here $P$ and $Q$ are fixed types (free type variables). We only consider pure lambda terms in ...
- 697
12
votes
1
answer
658
views
A type theory for curried functions with named/labeled arguments
I am not sure which stackexchange site is the best one to ask this question on; please tell me if you think it should go somewhere else.
Many programming languages have a notion of named or labeled ...
- 817
2
votes
1
answer
208
views
What did Backus mean by "housekeeping" here
In J. Backus's Can Programming Be Liberated from the von Neumann Style? A Functional Style and Its Algebra of Programs (1977), section 5.1, he wrote,
...
- 141
1
vote
0
answers
73
views
Resources for implementing a minimal, functional SMT lib-compliant SMT solver?
Title. Looking to build an experimental, minimal, functional, and pure SMT solver that hooks into the backends of Dafny and Verus. I'm happy using or looking into any functional programming language ...
- 29
3
votes
3
answers
221
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:
...
- 131
3
votes
2
answers
256
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 ...
- 697
5
votes
0
answers
208
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 ...
- 697
2
votes
1
answer
169
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 ...
- 123
4
votes
3
answers
393
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. ...
- 697
4
votes
1
answer
286
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 ...
- 668
1
vote
0
answers
92
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",...
- 990
0
votes
0
answers
122
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. ...
- 127
4
votes
2
answers
519
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 ...
- 43