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
1 vote
1 answer
28 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
0 votes
0 answers
13 views

Co-refinement or PER-refinement types

I just learned about LiquidHaskell, which is Haskell with refinement types. As pointed out by drcicero, the type former that sets apart a refinement type system from a simple type system is the type ...
  • 101
0 votes
0 answers
24 views

Exercise from Algebra of Programming on catamorphisms

This is an exercise from Algebra of Programming which I'm reading for self-study. Below, $T$ is the initial algebra of $F$. What I've tried: I can construct $h \circ F (\pi_2) : F(A \times B) \...
  • 223
7 votes
1 answer
669 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
258 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
39 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
61 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
35 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.
1 vote
1 answer
149 views

GroupBy key a sequence of ordered key values

I have a sorted (by key) sequence of key value pairs: ...
1 vote
1 answer
53 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,382
8 votes
3 answers
238 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,382
1 vote
1 answer
209 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
154 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 ...
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 ...
3 votes
1 answer
181 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
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 ...
1 vote
1 answer
142 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
0 votes
1 answer
107 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 ...
0 votes
0 answers
32 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
1 vote
0 answers
112 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....
2 votes
2 answers
136 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 :...
4 votes
1 answer
193 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 ...
0 votes
1 answer
83 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: ...
1 vote
1 answer
216 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 ...
1 vote
0 answers
42 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
27 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
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 ...
  • 21
9 votes
1 answer
533 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 ...
  • 141
10 votes
1 answer
411 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 ...
  • 211
1 vote
0 answers
139 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 ...
4 votes
1 answer
80 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. ...
1 vote
0 answers
57 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 ...
5 votes
1 answer
381 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 ...
2 votes
1 answer
385 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: ...
  • 593
0 votes
0 answers
44 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 ...
  • 593
13 votes
1 answer
285 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
182 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 ...
  • 477
3 votes
1 answer
134 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 ...
  • 477
4 votes
1 answer
290 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 ...
0 votes
1 answer
243 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 \...
1 vote
0 answers
179 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 ...
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 ...
0 votes
1 answer
669 views

“Left identity” of Monad laws in Haskell is wrong

Monad laws in Haskell ...
  • 111
3 votes
1 answer
245 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 ...
1 vote
1 answer
285 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 ...
4 votes
2 answers
356 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 ...
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 ...
4 votes
1 answer
416 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&...
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 ...
  • 133
0 votes
1 answer
101 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: ...