# Tag Info

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 ...

6

The missing part is the "identity extension lemma", which is mentioned in Reynolds' original paper but not in Wadler's. For $F : \text{Type} \to \text{Type}$, this says that if the relational interpretation of $F$ is instantiated with a type $A$ and the identity relation on $A$, we get the identity relation on $F\,A$. For System F, identity ...

2

$[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

There are two senses in which type formation operations are 'functorial,' but neither matches functoriality on the category of types. First, you can interpret the collection of types as a groupoid, and consider isomorphisms between types to be 'arrows.' These compose, but also always have inverses, so are in some sense undirected. However, this is also why ...

1


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-...

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