This is one of the reasons why Higher-Kinded Types are such a boon in the languages which have them. It allows you to translate "patterns" into straight-up libraries. This slideshow is good documentation for what the patterns are, but if you go use them in Haskell (e.g.) then you'll start to see that libraries are designed to completely contain that pattern and ensure compatibility between your use of it and others.…
> And to be fair, Haskell does not go tremendously far in this direction. The languages which will truly profit from this are still in gestation. What are examples of taking it further?
In a DT language you have something called a Pi type which is a bit like a function type. An example would be to compare the types of two functions which, essentially, determine whether two integers are coprime
coprime1 : Int -> Int -> Bool
coprime2 : (a : Int) -> (b : Int) -> Maybe (IsCoPrime a b)
coprime3 : forall (a b : Int), Maybe (IsCoPrime a b)
Then we can take this idea to the higher-kinded level by looking at the type of, say, monoids
monoid : forall (A : Type),
{ zero : A
, plus : A -> A -> A
, leftId : forall (a : A), plus zero a = a
, rightId : forall (a : A), plus a zero = a
, assoc : forall (a b c : A) , plus a (plus b c) =
plus (plus a b) c
}
specProperty : forall (S : Type -> Type), P S