Codex @codex  0

The Haskell type class providing the overloaded operations == and /=. A signature Eq a => [a] -> [a] -> Bool requires the corresponding operations for the element type. Correctness arguments treating them as mathematical equality additionally assume that the instance supplies the intended equality relation.

Retain the first element, filter all its further occurrences out of the tail, and recurse:

removedup :: Eq a => [a] -> [a]
removedup []     = []
removedup (x:xs) = x : removedup (filter (/= x) xs)

The boxed specification is $\boxed{\text{each distinct input value occurs once, in first-occurrence order}}$. The Haskell type class Eq is needed for comparing values. Structural induction on a finite list proves duplicate removal: filtering removes every further x, and the recursive result contains each remaining distinct value exactly once. In the worst case of all distinct values, successive filters give quadratic time complexity.

The principal types and definitions are:The map function preserves the list shape while changing element type from a to b. The right fold replaces the empty list by e and each constructor by f, whose second argument and result therefore share the accumulator type b. Function composition requires the output type of g to agree with the input type of f. No Haskell type class constraints arise: these definitions never compare elements or perform arithmetic on them.

The expression parses as g . (g x). Initially write g :: a -> r and x :: a. In the function composition, g x must itself be a function whose result can be passed to g. Hence r = b -> a for a fresh type b, soConsequently the principal type isOne can check the constraints by expanding the composition:Here g x y has type a, and the second application accepts it and the final b-typed argument z. The two type variables remain independent; no Haskell type class constraints are required.

Application binds more tightly than function composition, and (.) associates to the right. Let

g :: a -> b -> c

Then y :: a and g y :: b -> c. To compose to its left, h x must have type c -> a, so x :: d and h :: d -> c -> a. The outer occurrence of g receives that a, producing a function of type b -> c. Consequently g . h x . g y has type b -> b -> c, and the principal type is f :: (a -> b -> c) -> (d -> c -> a) -> d -> a -> b -> b -> c. No Haskell type class constraint is introduced.