Questions tagged [haskell]
The haskell tag has no usage guidance.
22
questions
2
votes
0
answers
100
views
Does GHC use graph reduction?
I have read somewhere that GHC does not use graph reduction for compiling/evaluating expressions. Is this right? If yes, what does it use as an alternative?
- 131
0
votes
1
answer
129
views
Why can't opaque optics form a category?
The optics Haskell package is an alternative to the famous lens package.
lens uses a van ...
- 111
2
votes
2
answers
328
views
Uncountability in intuitionistic logic
I've read snippets here and there that inside intuitionistic logic, uncountable can be a subset of the naturals ?
What is the correct intuition to think about this? Andrej Bauer replied above, saying ...
- 595
4
votes
1
answer
466
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 ...
- 141
4
votes
1
answer
180
views
What are values relative to Hask?
According to ncatlab's page on category theory and haskell,
"we can identify a subset of Haskell called Hask that is often used to identify concepts used in basic category theory. One considers ...
- 433
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 ...
9
votes
1
answer
357
views
A bicartesian closed category of strict complete partial orders (Hask)
It seems to be well-known that programming languages can't have sums, products and nontermination together.
Q1. Is this true? Below (or in the above link I gave) is a partial argument.
However, ...
- 2,049
1
vote
1
answer
201
views
Is the topsort from "Structuring Depth-First Search Algorithms" guaranteed to be (reverse) stable?
In "Structuring Depth-First Search Algorithms in Haskell", implemented in Data.Graph in the Haskell standard library, an algorithm for topologically sorting graphs is given:
...
- 213
1
vote
2
answers
2k
views
How to implement a functional programming language efficiently?
Thanks to Petr and Andrej for their feedback.
I'm rephrasing my question and give a bit of a context:
Functional programming languages are mostly based on lambda calculus.
Implementing a functional ...
user36006
1
vote
1
answer
177
views
Are the `ArrowApply` and `Monad` typeclasses equivalent?
It is stated e.g. on Hackage, that the ArrowApply and the Monad typeclasses are equivalent. I have my doubts about this.
It is ...
- 584
32
votes
2
answers
3k
views
What functions can System F not compute?
In this wikipedia article on Turing Completeness it states that:
The untyped lambda calculus is Turing complete, but many typed lambda calculi, including System F, are not. The value of typed ...
- 373
3
votes
0
answers
544
views
Distributive law between monads in Haskell
A distributive law between monads must satisfy laws that are usually given in terms of the units $\eta$ and multiplications $\mu$ of the two monads. Among the four laws there are:
$\mu^S T \circ S l \...
- 381
4
votes
2
answers
280
views
Can programming help one understand constructive mathematics?
I have read about the principles of constructive mathematics, for example, the principle of excluded middle is not allowed, and now I want to do some exercises to increase my understanding of the ...
- 121
25
votes
5
answers
2k
views
Are there any annotated formal verification systems for pure functional programming languages?
ACSL (Ansi C Specification Language), is a specification for C code, annotated with special comments, that allows C code to be formally verified.
I have not looked into it, but I imagine that the ...
- 603
11
votes
4
answers
1k
views
Explaining monad transformers in categorical terms
Most resource regarding categorical notions in programming describe monads, but I've never seen a categorical description of monad transformers.
How could monad transformers be described in the terms ...
- 2,571
6
votes
0
answers
273
views
Generalizing Haskell: could we replace Hask with Cat?
N.B. I asked the same question on Stack Overflow but it was suggested that it is too theoretical for this forum.
It is great that Haskell allows us to walk around in the category $Hask$. But ...
- 381
8
votes
1
answer
1k
views
Practical implementation of Hindley–Milner with typeclasses — matching vs most general unifier
I'm trying to get a deep understanding of a (great) paper "Typing Haskell in Haskell". I'm having difficulties understanding the implementation of two methods there — the ...
- 211
6
votes
3
answers
491
views
Isomorphism between algebraic data-types
I have two types of trees in Haskell, defined as the least solution of the following equations:
$T_1(A) \cong 1 + A + T_1(A) \times T_1(A)$
$T_2(A) \cong 1 + A \times T_2(A) + T_2(A) \times T_2(A)$
...
- 71
14
votes
4
answers
861
views
Is eta-equivalence for functions compatiable with Haskell's seq operation?
Lemma: Assuming eta-equivalence we have that (\x -> ⊥) = ⊥ :: A -> B.
Proof: ⊥ = (\x -> ⊥ x) by eta-equivalence, and <...
- 618
4
votes
1
answer
423
views
Aren't Monads F-Algebra's? And then if that could be said are Comonad's F-Coalgebra's?
So considering a Monad to be a Triple (T:C -> C, η, µ) with eta and mu as the Natural transformations with appropriate signatures, isn't this in essence an F-Algebra?
My thinking is that being both (...
- 143
4
votes
0
answers
198
views
Type-and-effect systems, stochasticism and effect squelching: how about quicksort?
There's a feature of Haskell's type system which bugs me: you can't implement a randomized sorting algorithm without the use of randomness spilling out into all of its callers. That seems undesirable....
- 249
12
votes
2
answers
762
views
What are the relations between Alternative, MonadPlus(LeftCatch) and MonadPlus(LeftDistributive)?
Following up What’s an example of a Monad which is an Alternative but not a MonadPlus?:
Assume $m$ is a monad. What are the relations betweem $m$ being an Alternative, a MonadPlusCatch and a ...
- 2,571