Generally what we're talking about is the ability to say something like "for all types X which satisfy a predicate P, we have this code". The ability to quantif

Generally what we're talking about is the ability to say something like "for all types X which satisfy a predicate P, we have this code". The ability to quantify over "all" types is a key property of dependently typed languages. Likewise, a lot of Haskell's ability to simulate DT languages comes from its ability to reason about HKTs. 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) The important part is to look past the syntax and note that IsCoPrime is a type which depends upon the values of the first two arguments. Another way of reading this is as follows coprime3 : forall (a b : Int), Maybe (IsCoPrime a b) this emphasizes that the type of `coprime3` is quantifying over all values in Int. 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 } Here we can see that the `forall` notation lets us freely abstract over "all types" just like we previously abstracted over "all values". This continues to work at every level. For instance, we can note that `monoid` above is "a type of types" or maybe a "specification" and we can abstract over all "all specifications" as well specProperty : forall (S : Type -> Type), P S