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

54 questions
Filter by
Sorted by
Tagged with
248 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). ...
907 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 ...
263 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 ...
495 views

### Curry Howard correspondence to Predicate Logic?

So I'm trying to get my head round Curry-Howard. (I've tried at it several times, it's just not gelling/seems too abstract). To tackle something concrete, I'm working through the couple of Haskell ...
171 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 ...
153 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 ...
366 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 on the ...
721 views

### Are there any type constructors which are *not* functors?

So I'm almost done teaching myself category theory. One of the main take-aways for me is that type constructors (higher-kinded types) are endo-functors. But it this always the case? What's throwing ...
393 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 ...
356 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 ...
171 views

42 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. ...
241 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 ...
317 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&...
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 ...
169 views

### Can Haskell ensure a Functor (or other typeclasses) satisfies its law?

It seems that Functor definitions in Haskell can be accepted if the type is correct. This code compiles, but it doesn't satisfy the functor law: ...
105 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 ...
64 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 ...
213 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 ...
87 views

85 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 ...
587 views

### Calculating mean, min, max, sum of a list of integers - what's the complexity?

This is sort of a silly question that's been bugging me. I have a list of 100k numbers that I am calculating some statistics for. Specifically, I am computing the mean, minimum, maximum, and sum of ...
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 ...
151 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: ...
83 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 ...
117 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 ...
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 ...
73 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 ...
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 ...
227 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 ...
109 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 ...
90 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 :...
73 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 ...
94 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....
39 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,...
103 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 ...
49 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 ...
168 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 ...
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 ...
522 views

175 views

56 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: ...
89 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: ...