Hot answers tagged

12

A monad in Haskell is intended to be a monad on the category of types, when the category theory is done internally to the type theory. The capabilities of Haskell and similar languages are somewhat limited, so there are a lot of basic constructions in category theory that cannot be done, but there are plenty of structures that can be encoded reasonably. M ::...


7

Performance is not a property of language, it is a property of specific programs within a language. Some languages might be very fast at some things and slow at others. For example, Chez-Scheme can sometimes find performance comparable to C, not because the language is more efficient, but because defensive practices that programmers often use in C are less ...


6

I would find a different tutorial because the author of that one is fundamentally confused. They wrongly claim that $\neg a$ and $\bot\to a$ are equivalent ($a\to\bot$ would be correct), and also wrongly claim that you can't write a function of type $\texttt{Void}\to a$. $\texttt{Void}\to a$ is vacuously true. In principle a function of that type should ...


1

You are looking for Church encodings of datastructures in $\lambda$-calculus, and in particular of lists.


1

$[3,2,1]$ is just syntactic sugar for $\mathsf{cons} \, 3 \, (\mathsf{cons} \, 2 \, (\mathsf{cons} \, 1 \, \mathsf{nil}))$. $[3,2,1]$ is $\mathsf{cons} \, 3 \, [2,1]$ by definition of the $[\ldots]$ notation. Because $\mathsf{cons}$ is part of the definition of lists, it isn't meaningful to ask whether $\mathsf{cons}$ is correct on its own. The meaningful ...


1

Composition following from identity does not hold for the category of sets and functions (to my knowledge), if by that you mean the sets and functions in ZF(C) or the like that mathematicians usually consider. As you mentioned, the given argument relies on parametricity, and the functions definable in set theory needn't be parametric. In fact, assuming that ...


1

The thing to notice here is that your function sum is defined on lists, which are inductively defined. Theoretically, the inductive definition of a list defines for every type T a term match_list :: T -> (a -> [a] -> T) -> ([a] -> T) satisfying the property match_list s t [] = s match_list s t (x::xs) = (t x xs) in addition, defining a ...


1

Look at Agda [1][2] I think that it's exactly what you are looking for. I recommend using its emacs mode for autocompletion and hole/interactive programming. [2]/quick-guide.html A very good introduction is plfa [3], also [2]/tutorial-list.html [1] https://en.wikipedia.org/wiki/Agda_(programming_language) [2] https://agda.readthedocs.io/en/v2.6.0.1/getting-...


1

Contrary to Church's lambda calculus, Haskell is typed. Answer 1 When types are denoted with lower-case letters (such as p1 and p2) that indicates a type variable. When types are denoted with capital letters (e.g. Bool or Int) they're concrete types. The type p1 -> p2 -> p2 indicates a function in curried form. You can think of it as a function that ...


1

Here is a provisional answer. The de Bruijn index and level of a bound variable sum up to the number of enclosing lambdas: $i+l=n_\lambda$. Since the index can be recovered from the level by subtraction, levels can be implemented as 'predecessor' indices p: z :: (a, b) -> a z (x, _) = x s :: (a -> b) -> (c, a) -> b s v (_, h) = v h -- ^^^ as ...


Only top voted, non community-wiki answers of a minimum length are eligible