Questions tagged [haskell]

Haskell is a functional programming language featuring strong static typing, lazy evaluation, extensive parallelism and concurrency support, and unique abstraction capabilities.

Filter by
Sorted by
Tagged with
0 votes
2 answers
209 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: ...
user avatar
2 votes
1 answer
35 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 ...
user avatar
  • 121
0 votes
1 answer
49 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 <...
user avatar
  • 109
0 votes
1 answer
32 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.
user avatar
1 vote
1 answer
140 views

GroupBy key a sequence of ordered key values

I have a sorted (by key) sequence of key value pairs: ...
user avatar
1 vote
1 answer
49 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 ...
user avatar
  • 3,464
7 votes
2 answers
207 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 ...
user avatar
  • 3,464
1 vote
1 answer
205 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 ...
user avatar
2 votes
1 answer
125 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 ...
user avatar
11 votes
1 answer
1k 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 ...
user avatar
3 votes
1 answer
166 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 ...
user avatar
  • 555
0 votes
0 answers
93 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 ...
user avatar
1 vote
1 answer
131 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 ...
user avatar
  • 145
0 votes
1 answer
93 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 ...
user avatar
0 votes
0 answers
31 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 ...
user avatar
  • 101
1 vote
0 answers
104 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....
user avatar
2 votes
2 answers
122 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 :...
user avatar
4 votes
1 answer
184 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 ...
user avatar
0 votes
1 answer
72 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: ...
user avatar
1 vote
1 answer
167 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 ...
user avatar
1 vote
0 answers
41 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,...
user avatar
  • 253
0 votes
0 answers
26 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,...
user avatar
2 votes
0 answers
25 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 ...
user avatar
  • 21
9 votes
1 answer
503 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 ...
user avatar
  • 141
10 votes
1 answer
383 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 ...
user avatar
  • 211
1 vote
0 answers
133 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 ...
user avatar
4 votes
1 answer
70 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. ...
user avatar
1 vote
0 answers
55 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 ...
user avatar
5 votes
1 answer
373 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 ...
user avatar
2 votes
1 answer
336 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: ...
user avatar
  • 593
0 votes
0 answers
43 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 ...
user avatar
  • 593
12 votes
1 answer
278 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). ...
user avatar
  • 223
0 votes
0 answers
166 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 ...
user avatar
  • 477
3 votes
1 answer
128 views

An Alternative History of Haskell: being lazy without class?

[The q is a play on the title of this 2007 survey of Haskell.] tl;dr I have a couple of connected questions about Haskell's overloading mechanisms. I'll ask first then explain why. I'm looking at the ...
user avatar
  • 477
4 votes
1 answer
280 views

Typing rule for binding groups

In "Typing Haskell in Haskell", by Mark P. Jones, is provided a sort of haskell-like specification for typing Haskell. As stated in this paper, binding groups is a area "neglected in most theoretical ...
user avatar
0 votes
1 answer
230 views

Can this set of propositions be represented and proved in Haskell?

I used a set of natural language statements and their formalization from Gries and Schneider. I attempted to transform the propositions into Haskell equations. For example, for S0 : $a \land w \...
user avatar
1 vote
0 answers
176 views

Does this Haskell code represent a decision procedure for a theorem?

The following is a natural language description of a first order theory from Worboys. Only Axiom 11 and the Theorem 4 are written in mathematical notation. Theory 1 Aland, Bland, Cland, and Dland are ...
user avatar
1 vote
1 answer
1k views

Is Pattern Matching as expressive as Case Expression in Haskell?

Nomenclature The term expressive in the question shall bear the same meaning as in the following sentence: A Turing Machine is as expressive as Lambda Calculus. Introduction While learning ...
user avatar
0 votes
1 answer
614 views

“Left identity” of Monad laws in Haskell is wrong

Monad laws in Haskell ...
user avatar
  • 111
3 votes
1 answer
237 views

Relating a proof to a Haskell program

I am trying to relate the following integer square root theorem $\forall x: \mathbb{N}, \exists y : \mathbb{N}((y^2 \leq x) \land (x < (y+1)^2))$ and its proof to its role as a specification of ...
user avatar
1 vote
1 answer
270 views

Haskell type class and initial algebra

For the example below, I am trying to understand how Haskell type classes, type class instances, and data types relate to the concept of initial algebra. There are two Haskell data types sharing a ...
user avatar
4 votes
2 answers
336 views

In Hindley-Milner system, how can I prove that let id=\x.x in id id is well-typed?

I am trying to infer the type and prove that this is well-typed: let $f =\lambda x.x$ in $f f$ Obviously the $f$ is the identity function, so it's the same as let $id =\lambda x.x$ in $id$ $id$ I ...
user avatar
2 votes
1 answer
35 views

Unclear logic notation for PFX program rules

I'm very new to this so please bear with me. I found this document describing the PFX language, a stack-oriented language where the instructions act on a stack and replace the arguments with the ...
user avatar
4 votes
1 answer
397 views

Haskell type classes as ontological categories

A paper uses Haskell type classes to represent ontological categories. A type class hierarchy is used to represent "concept hierarchies" where "functions are the units of inheritance&...
user avatar
3 votes
1 answer
71 views

How should I describe the relationships between type expressions?

Lets say I have two type expressions: Maybe a (X) and Maybe Integer (Y), where Maybe is a ...
user avatar
  • 133
0 votes
1 answer
99 views

Understanding arguments in Haskell type classes and instances

I am trying to understand a Haskell class declaration and instance from a paper. I am trying to understand the class declaration: ...
user avatar
6 votes
1 answer
178 views

How to model conditionals with first-class functions?

Since languages with recursible first-class functions are Turing-complete, they should be able to express anything expressible in any other programming language. Therefore, it should be possible to ...
user avatar
0 votes
1 answer
139 views

Can we define the Functor Category in Haskell (or any other language with a more expressive type system)?

Here I am talking about the Functor category, which is defined as a category whose objects are functors and morphisms are natural transformations. For reference: https://ncatlab.org/nlab/show/functor+...
user avatar
3 votes
2 answers
79 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 ...
user avatar
5 votes
1 answer
414 views

Implementing mathematical theory of arithmetic in Haskell via Curry-Howard correspondence

I have to ask for forgiveness in advance if the whole question doesn't make a lot of sense, but unfortunately, I have no better intuition as of right now and this seems like the best starting point I ...
user avatar