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
1answer
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.
1
vote
1answer
123 views

GroupBy key a sequence of ordered key values

I have a sorted (by key) sequence of key value pairs: ...
1
vote
1answer
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 ...
7
votes
2answers
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 ...
1
vote
1answer
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 ...
2
votes
1answer
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 ...
10
votes
1answer
965 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
1answer
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 ...
0
votes
0answers
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 ...
1
vote
1answer
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 ...
0
votes
1answer
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 ...
0
votes
0answers
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 ...
1
vote
0answers
99 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....
1
vote
2answers
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 :...
2
votes
1answer
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 ...
0
votes
1answer
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: ...
1
vote
1answer
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 ...
1
vote
0answers
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,...
0
votes
0answers
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,...
2
votes
0answers
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 ...
8
votes
1answer
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 ...
10
votes
1answer
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 ...
1
vote
0answers
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 ...
4
votes
1answer
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. ...
1
vote
0answers
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 ...
5
votes
1answer
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 ...
2
votes
1answer
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: ...
0
votes
0answers
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 ...
12
votes
1answer
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). ...
0
votes
0answers
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 ...
3
votes
1answer
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 ...
4
votes
1answer
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 ...
0
votes
1answer
201 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
0answers
171 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
1answer
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
1answer
556 views

“Left identity” of Monad laws in Haskell is wrong

Monad laws in Haskell ...
3
votes
1answer
229 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
1answer
249 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
2answers
313 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
1answer
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 ...
4
votes
1answer
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&...
3
votes
1answer
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 ...
0
votes
1answer
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: ...
6
votes
1answer
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 ...
0
votes
1answer
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+...
3
votes
2answers
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 ...
5
votes
1answer
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 ...
1
vote
0answers
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 ...
3
votes
3answers
175 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: ...
3
votes
1answer
101 views

How to explain/understand brackets of applicative functor [[f u1... un]]?

I am reading article about Applicative Abstract Categorial Grammars http://okmij.org/ftp/gengo/applicative-symantics/AACG.pdf and this article uses brackets [[...]] for action on terms inside ...