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

56 questions
Filter by
Sorted by
Tagged with
26 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.
123 views

### GroupBy key a sequence of ordered key values

I have a sorted (by key) sequence of key value pairs: ...
43 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 ...
186 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 ...
172 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 ...
94 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 ...
965 views

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 ...
137 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 ...
92 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 ...
110 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 ...
69 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 ...
28 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 ...
99 views

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....
102 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 :...
150 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 ...
64 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: ...
106 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 ...
40 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,...
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,...
24 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 ...
422 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 ...
328 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 ...
115 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 ...
50 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 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 ...
363 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 ...
251 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: ...
42 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 ...
262 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). ...
122 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 ...
122 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 ...
260 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 ...
201 views

32 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 ...
358 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&...
67 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 ...
97 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: ...
163 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 ...
134 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+...
77 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 ...
403 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 ...
50 views

### How can I prove impossibility of generalizing a given higher order function from pure to monadic or applicative?

There is a great divide in Haskell between pure and monadic algorithms. While the latter are indistinguishable from their usual imperative counterparts, the former can get much more magical. What this ...