Questions tagged [haskell]
Haskell is a functional programming language featuring strong static typing, lazy evaluation, extensive parallelism and concurrency support, and unique abstraction capabilities.
76
questions
1
vote
0
answers
26
views
Is there any reference materials on complexity analysis for lazy languages?
Is there any books, papers or articles on how to analyze the time complexity of programs written in lazy languages such as Haskell?
I know how laziness is implemented and how it can be expanded and ...
0
votes
0
answers
57
views
Representation of pairs in System F
System F defines the data type pair as:
$$X\times Y := \Pi Z. (X\to Y \to Z)\to Z$$
with:
$$\langle x,y \rangle := \Lambda Z. \lambda p^{X\to Y\to Z}.p \text{ }x\text{ } y$$
Projections are defined:
$$...
1
vote
1
answer
60
views
DFA for even concatenation of strings from a language
If I have a deterministic finite automaton (DFA) with a language $W$, and I need to create another DFA that returns all the strings that are a concatenation of an even number of strings in $W$, how ...
- 11
2
votes
1
answer
60
views
Are Haskell monads stronger than strong monads?
Haskell's monads are usually considered to mean strong monads in category theory, but it seems like the former is a bit stronger than the latter. With strong monads, you have a Kleisli extension ...
- 123
1
vote
0
answers
33
views
Mathematical explanation of the usage of monads to wrap data for avoiding errors
For the past two days I have been on a question to understand monads in the context of Haskell. A nice explanation I found is by Graham Hutton on the Computerphile channel see here. This explanation ...
1
vote
0
answers
35
views
How much is decidability compromised within this restriction of the fixpoint combinator?
Though purely functional programming languages, such as Haskell, is commonly thought to have no side-effects, there is a caveat: Recursive calls may hang.
I considered this to be undesirable, and ...
- 335
1
vote
1
answer
43
views
Literature on delta encoding serializeable ADTs
Suppose that I have some nested algebraic data type (ie. something one can construct via datas in Haskell) that is serializeable (so no functional fields ...
- 41
1
vote
0
answers
37
views
What is the type of a type signature?
For example, using GHCi,
ghci> f x = x + 1
ghci> :t f
f :: Num a => a -> a
What is the type of the type signature ...
7
votes
1
answer
685
views
Strictness in both arguments but not in each individually
I'm learning about strict functions in Haskell.
A function f is strict if f ⊥ = ⊥
Some functions are strict only in the first argument (for e.g. const), others are strict in the second (for e.g. map)....
- 73
4
votes
1
answer
69
views
Book references for combinatory logic as applied in Haskell?
I am looking for book references on combinatory logic. Is there a book focused on how combinatory logic is applied in the context of pure functional languages like Haskell?
I found "Combinators: ...
0
votes
0
answers
10
views
Up-to-date status of the GHC STG?
Where can I read about the current status of the GHC STG?
The paper that I have is "Implementing Lazy Functional Languages on Stock Machine: the Spineless Tagless G-machine". For example, I ...
- 109
0
votes
0
answers
52
views
If type theory is one of the foundation of Haskell, why can't you call a function in itself?
Consider this following Lambda expression:
$$\lambda s. (s \text{ } s )$$
This function applies it's arguement to it's arguement. If this is a valid lambda expression, wouldn't it also be allowed in ...
0
votes
0
answers
35
views
Ambiguous type of "triangle" operator for sum types
In Meijer, Fokkinga and Patersons "Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire" the ∇ operator for sum types is introduced which removes the tags from its ...
- 26
0
votes
0
answers
55
views
Is type inference for arbitrary-rank types decidable when supplied type signatures?
I found following statements in 6.4.16. Arbitrary-rank polymorphism of ghc document.
GHC uses an algorithm proposed by Odersky and Laufer (“Putting type annotations to work”, POPL‘96) to get a ...
- 13
2
votes
2
answers
172
views
The second Functor law is redundant, but I don't understand the proof
When we defining a Functor instance in Haskell, it should satisfy the following two laws:
fmap id = id
...
- 123
1
vote
1
answer
59
views
How does GHC insert type abstraction/application under the RankNTypes extension
I'm developing a functional programming language that offers Rank-n polymorphism. Like Haskell I don't want types to appear at the term level, but I have no idea to insert type abstraction and type ...
- 13
7
votes
1
answer
1k
views
What exactly is the relation between Haskell and category theory?
In articles or Quora posts about category theory, I often find mentions of the programming language Haskell. I have little knowledge of category theory and even less of programming. Could someone ...
0
votes
2
answers
515
views
Algorithm for Getting Largest Connected Component From List of Touching Pairs
I have a program which finds the touching pairs of a given value in a binary image. For example, consider the below image:
...
2
votes
1
answer
40
views
What is the meaning of "You describe the result you want rather than specifying the steps required to get there." in Functional Programming?
One of the characteristics of functional programming is as follows:
You’re describing the result you want rather than explicitly specifying the steps required to get there.
I found this quote at ...
- 121
0
votes
1
answer
211
views
Implementing a correct `let rec in` interpreter in Haskell with `eval` and `sub` semantics
I'm implementing the toy fb-lang from the principles of programming language book. It's a small interpreted language that uses eval(uate) expression function and <...
- 109
0
votes
1
answer
37
views
Pure Directed Graph
How can a directed graph be efficiently represented in a purely functional language like Haskell? Could someone suggest relevant materials on this topic? (functional pearls perhaps?) Thanks.
- 347
1
vote
1
answer
169
views
GroupBy key a sequence of ordered key values
I have a sorted (by key) sequence of key value pairs:
...
- 45
2
votes
2
answers
77
views
Can we somehow get functoriality from purely type-theoretic reasoning?
In this question, I asked about how to prove naturality from parametric polymorphism, using parametricity. The current answer to that question simply assumes that the functors in question satisfy the ...
- 3,652
10
votes
3
answers
394
views
Rigorous proof that parametric polymorphism implies naturality using parametricity?
This question asks for an informal explanation of why all polymorphic functions between functors are natural transformations (This is a claim made by Bartosz Milewski). One answer to that question ...
- 3,652
1
vote
1
answer
228
views
λ -terms that correspond to Haskell functions
Evening All
I already have a "grasp" of haskell (not terrible, about 6 month experience) and am trying to learn the fundamentals that sit behind it, thus am now turning my attention to ...
user130129
2
votes
1
answer
293
views
Show that term cons works by showing all beta reductions
I'm new to functional programming.
So the terms cons appends an element to the front of the list. Where cons ≜ λx:λl:λc:λn: c x (l c n).
How should I go about proving that cons works correctly using ...
- 23
11
votes
1
answer
2k
views
Monad in Haskell programming vs. Monad in category theory
I have a question about concept of monad used in Haskell programming
and category theory in math.
Recall in Haskell a monad consists of following components:
A type constructor that defines for each ...
- 223
3
votes
1
answer
250
views
Curry-Howard, void, and type checking in Haskell
I am trying to understand an example of theorem proving via type checking in Haskell given here. The example is as follows.
Using the Curry-Howard isomorphism, construct an inhabitant of the type and ...
- 565
0
votes
0
answers
96
views
Can we think of a non-symmetric product type in Haskell?
Meta note: I asked this question here a while ago. It got an answer:
type a /\!! b = (a, ((b -> Void) -> Void))
Unfortunately, I do not reckon it to be ...
- 228
1
vote
1
answer
206
views
For every imperative function, is there a functional counterpart with identical performance or even instructions?
Currently, I haven't learned about a functional language that can achieve the same performance as C/C++. And I have learned that some languages that favor functional programming to imperative ...
- 145
1
vote
1
answer
185
views
Functor in category theory: The free theorem for fmap
According to nLab article:
https://ncatlab.org/nlab/show/functor
Definition
External definition
A functor $F$ from a category $C$ to a category $D$ is a map sending each object $x \in C$ to an object ...
- 113
0
votes
0
answers
37
views
Is my understanding of strictness correct in this proof of a `foldl` rule?
Exercise G in Chapter 6 of Richard Bird's Thinking Functionally with Haskell asks the reader to prove
foldl f e . concat = foldl (foldl f) e
given the rule
...
- 101
2
votes
1
answer
171
views
How do type classes make ad-hoc polymorphism less ad hoc?
The title of the paper that introduced type classes is "How to make ad-hoc polymorphism less ad hoc".
It seems the type classes approach is being compared to how OOP does ad-hoc polymorphism....
- 346
2
votes
2
answers
286
views
Lambda Calculus Conversion
How can I take a Haskell data type or function (eg fold, list, String, zip) and convert or translate it to a lambda calculus abstraction?
Example:
If sum computes a sum of all elements in a list, and
:...
- 123
4
votes
1
answer
269
views
How to view Graph Reduction/Graph Representation for a Haskell program?
I know that under the hood, for a Haskell program, the GHC compiler uses graph reduction for optimization. Is there any way to view this graphical representation of the program? I haven't been able to ...
- 41
1
vote
3
answers
230
views
Prove simple theorems in Haskell in automated way
I would like to prove in Haskell, whether in vanilla Haskell or using some libraries / tools, some simple theorems such as:
...
2
votes
1
answer
422
views
Haskell type of lambda expressions
I'm new to Haskell and have some general questions.
Question 1:
The Haskell expression (\x -> \x -> x) is the same as the λ-term ...
- 21
1
vote
0
answers
44
views
Is the identity functor a kind of free object?
My understanding of free objects is: Free functors, free applicatives, free monads, free monoids, &c, give you more structure "for free", i.e. in general, or for all some thing with less structure,...
- 253
0
votes
0
answers
29
views
Haskell: difference behavior in ghci concerning ``polymorphic recursion''
I stumbled upon some question that puzzled me, maybe it's just a feature
(or simply because I am doing first ``Haskell-steps'' without studying the
manual too deeply, which I guess I should...
Anyway,...
2
votes
0
answers
26
views
Is possible to construct a fixed set of typeclases as powerful as unconstrainde typeclasses?
We can construct a fixed set of combinators with a computational power equivalent to lambda calculus.
Can we do the same with typeclasses (ad-hoc polymorphism)?
For example, construct a finite set ...
- 21
9
votes
2
answers
711
views
Functor laws and natural transformations in Haskell
As I've been struggling to get a deeper understanding of monads in Haskell, I started reading about functors and their counterparts in category theory. Keep in mind that I have no background in the ...
- 183
10
votes
1
answer
493
views
Semantics for de Bruijn levels
There is an exceptionally simple way to embed simply typed lambda calculus with de Bruijn indices in a functional host language (discussed by Carette, Kiselyov & Shan, and by Kiselyov). The ...
- 231
1
vote
0
answers
165
views
Predecessor function with recursive types
I am defining the type Nat of natural numbers a recursive sum type:
$$ Nat = \mu X. Unit \oplus X$$
Now, I have defined zero ...
- 239
5
votes
1
answer
120
views
How does Bifunctor in Haskell work?
I was reading 'Category Theory for Programmers' by Bartosz Milewski and got really confused by the implementation of bimap in Bifunctor typeclass.
...
- 53
1
vote
0
answers
58
views
A notion dual to a product type having a given type
Consider this class:
class Has record part where
extract :: record -> part
update :: (part -> part) -> record -> record
It captures the notion of ...
- 175
6
votes
1
answer
397
views
Why does higher-order abstract syntax need an inverse to define catamorphisms?
In the introduction to the colorfully-named Boxes Go Bananas: Encoding Higher-Order Abstract Syntax with Parametric Polymorphism, Washburn and Weirich describe a problem in traditional formulations of ...
- 304
2
votes
1
answer
601
views
How does the function to curry and uncurrying another function work?
The following is the code to curry or uncurry a function in Haskell:
...
- 621
0
votes
0
answers
46
views
Inferring the type of (f .) in Haskell
If we have the following in Haskell:
f x y = x + y
:type f
f :: Num a => a -> a -> a
then GHC would report ...
- 621
13
votes
1
answer
316
views
Is the IO monad technically incorrect?
On the haskell wiki there is the following example of conditional usage of the IO monad (see here).
...
- 233
0
votes
0
answers
222
views
Data types a la carte -- over-engineered?
I'm working through Swierstra's 2008 paper. I'm up to Section 3 eval addExample, just before 'Automating injections'. And boy! does it need automating.
Is it just ...
- 487