Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [haskell]

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

4
votes
1answer
124 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
88 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
137 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 ...
1
vote
1answer
144 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
0answers
48 views

Monads not with “flatMap” but “flatUnit”?

Monads in category theory is defined by triples T, unit, flat⟩. ...
-1
votes
1answer
199 views
3
votes
1answer
99 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
102 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 ...
3
votes
2answers
104 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
19 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 ...
0
votes
0answers
112 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". Here is a class ...
3
votes
1answer
49 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
0answers
36 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
118 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
73 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
68 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
219 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 ...
2
votes
0answers
36 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 ...
2
votes
3answers
70 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: ...
4
votes
1answer
50 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 ...
5
votes
1answer
131 views

Can the semantics of a numeric hierarchy be faithfully represented in Haskell?

I am trying to represent a fragment of a number hierarchy using the Haskell concepts of value, type, and type class. I would like the Haskell code to reflect the mathematical semantics $\vdash ((x \in ...
3
votes
0answers
312 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 ...
4
votes
2answers
94 views

When does a type generalise another type?

In languages like Haskell, with a Hindley-Milner type system, when does a type $t$ generalise a type $u$? I use the definition: $t$ generalises $u$ iff $\forall\ v: v \text{ unifies with } u \...
7
votes
1answer
354 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 ...
3
votes
1answer
171 views

Prove foldl fusion law

I have proven the foldr Fusion Law as follows: Given f is strict, f a = b and ...
5
votes
1answer
401 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 ...