
author: Las Safin
date: "20230113"
keywords:
 higher
 kinded
 type
 hkt
 gadt
 type
 family
 computation
 haskell
title: All you need is higher kinded types
...
```haskell
{# LANGUAGE BlockArguments #}
{# LANGUAGE DataKinds #}
{# LANGUAGE DerivingStrategies #}
{# LANGUAGE GHC2021 #}
{# LANGUAGE LambdaCase #}
{# LANGUAGE LiberalTypeSynonyms #}
{# LANGUAGE PatternSynonyms #}
{# LANGUAGE QuantifiedConstraints #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE UndecidableInstances #}
{# LANGUAGE UndecidableSuperClasses #}
{# OPTIONS_GHC fprintexplicitforalls fprintexplicitkinds #}
{# OPTIONS_GHC fnoshowvalidholefits fdefertypeerrors #}
{# OPTIONS_GHC Wall Wcompat Wredundantconstraints #}
import Data.Kind (Type)
import Data.Void (Void)
import Data.Functor.Identity (Identity (Identity))
import Unsafe.Coerce (unsafeCoerce)
```
This is a literate Haskellfile. You can open it in GHCi by doing the following:
```bash
curl O https://las.rs/blog/allyouneedishkts.lhs
nix develop impure expr \
'with import {}; mkShell {
buildInputs =
[(haskell.packages.ghc924.ghcWithPackages
(p: [ p.markdownunlit ])
)];
}' \
c ghci pgmL markdownunlit allyouneedishkts.lhs
```
Haskellers (and even worse, dependent type brained people) are prone to making
complicated types to maximise abstraction and correctness.
However, you might be surprised to know that you (technically) need nothing more than ADTs,
HKTs, and rankN types to do almost all of the magic you need.
**Core theorem**:
(Roughly) any valid Haskell term (or of a similar language) typed with type families and GADTs,
can be reformulated as a _semantically equivalent_ term that can be typed without type families and GADTs.
What do I mean with semantically equivalent?
When erasing types, the new term has the _same structure_,
modulo technically unnecessary wrappings using constructors
that ought to be newtype constructors.
(You could in fact aleviate this by adding more language features,
but that would ruin the point, unless there is a way of doing it
in a minimal way.)
## Type families → Data families
Type families in Haskell represent uncurriable functions that transform
one typelevel term into another typelevel term.
Let us consider the following trivial example:
```haskell
type family Not b where
Not 'True = 'False
Not 'False = 'True
```
It is in fact possible to transform the above into a _data family_,
and in fact turn any type family into a data family (or something equivalent
to avoid the limitation wrt. overlapping data family instances, see end of this post):
```haskell
type NotD :: Bool > (Bool > Type) > Type
data family NotD b k
newtype instance NotD 'True k = NotDTrue (k 'False)
newtype instance NotD 'False k = NotDFalse (k 'True)
```
How can this be true? The intuitive and informal proof is that, at the typelevel
terms of data kinds, though not types themselves, will **always be used to construct a type**.
We lose _no power_ (modulo GHC bugs and Haskell misfeatures) compared to the type family version.
In addition, since the data family uses newtype instances, the term can be kept representationally
equivalent.
Let us give an example:
```haskell
data Something (b :: Bool) where
SomethingInt :: Int > Something 'True
SomethingDouble :: Double > Something 'False
flipSomething :: Something b > Something (Not b)
flipSomething (SomethingInt n) = SomethingDouble $ fromIntegral n
flipSomething (SomethingDouble n) = SomethingInt $ truncate n
```
We can transform the above into the following:
```haskell
flipSomethingD :: Something b > NotD b Something
flipSomethingD (SomethingInt n) = NotDTrue $ SomethingDouble $ fromIntegral n
flipSomethingD (SomethingDouble n) = NotDFalse $ SomethingInt $ truncate n
```
In fact, we can even do the following:
```haskell
flipSomethingD' :: Something b > Something (Not b)
flipSomethingD' = unsafeCoerce flipSomethingD
```
You can try running the above function and confirm it works.
Representionally, it should be equivalent to `flipSomething` modulo GHC optimisations
that might be inhibitted due to the use of `unsafeCoerce`.
## Data families → GADTs
If you look at `NotD`, you might notice that it looks awfully like a GADT.
```hs
 :k NotD
type NotD :: Bool > (Bool > Type) > Type
 :t NotDTrue
pattern NotDTrue :: forall (k :: Bool > Type). k 'False > NotD 'True k
 :t NotDFalse
pattern NotDFalse :: forall (k :: Bool > Type). k 'True > NotD 'False k
```
In fact, we can formulate the exact same thing, except unfortunately
it turns into a _data type_, hence unnecessary constructor tags and wrappings
are added in the representation:
```haskell
type NotG :: Bool > (Bool > Type) > Type
data NotG b k where
NotGTrue :: k 'False > NotG 'True k
NotGFalse :: k 'True > NotG 'False k
flipSomethingG :: Something b > NotG b Something
flipSomethingG (SomethingInt n) = NotGTrue $ SomethingDouble $ fromIntegral n
flipSomethingG (SomethingDouble n) = NotGFalse $ SomethingInt $ truncate n
```
You can **not** do the `unsafeCoerce` trick on this to turn it back into
the original `flipSomething`, given that `NotG` is (unfortunately) not a newtype.
One thing to note is that we gain slightly more power by turning it into a GADT,
notably, we can match on `NotG b k` and thus find out what `b` is.
## GADTs → ADTs
We can also go from GADTs to normal ADTs using equality proofs instead:
```haskell
type NotE :: Bool > (Bool > Type) > Type
data NotE b k
= b ~ 'True => NotETrue (k 'False)
 b ~ 'False => NotEFalse (k 'True)
flipSomethingE :: Something b > NotE b Something
flipSomethingE (SomethingInt n) = NotETrue $ SomethingDouble $ fromIntegral n
flipSomethingE (SomethingDouble n) = NotEFalse $ SomethingInt $ truncate n
```
However, equalities in constructor constraints are also somewhat exotic.
We can remove them by instead using `Data.Type.Equality.:~:`, but that
is in turn defined using a GADT, which we want to avoid.
We turn to Leibniz equality:
```haskell
type (:~:) :: forall k. k > k > Type
newtype (:~:) a b = EqPrf (forall p. p a > p b)
refl :: a :~: a
refl = EqPrf id
absurd :: 'False :~: 'True > a
absurd _ = error "absurd"
type NotEL :: Bool > (Bool > Type) > Type
data NotEL b k
= NotELTrue (b :~: 'True) (k 'False)
 NotELFalse (b :~: 'False) (k 'True)
flipSomethingEL :: Something b > NotEL b Something
flipSomethingEL (SomethingInt n) =
NotELTrue refl $ SomethingDouble $ fromIntegral n
flipSomethingEL (SomethingDouble n) =
NotELFalse refl $ SomethingInt $ truncate n
ex :: Int
ex = case flipSomethingEL (SomethingDouble 4.2) of
NotELFalse _ (SomethingInt n) > n
NotELTrue prf _ > absurd prf
```
## Peano arithmetic example
What is a nontrivial example then?
```haskell
data Nat = Zero  Succ Nat
data Vec (n :: Nat) (a :: Type)
= VNil (n :~: 'Zero)
 forall n'. VCons ('Succ n' :~: n) a (Vec n' a)
data Plus (x :: Nat) (y :: Nat) (k :: Nat > Type)
= PlusZero (x :~: 'Zero) (k y)
 forall x'. PlusSucc ('Succ x' :~: x) (Plus x' ('Succ y) k)
newtype Flip (f :: a > b > Type) (y :: b) (x :: a)
= Flip (f x y)
twoBools :: Plus ('Succ 'Zero) ('Succ 'Zero) (Flip Vec Bool)
twoBools = PlusSucc refl $
PlusZero refl $ Flip $ VCons refl True $ VCons refl True $ VNil refl
```
Compared to the original approach where you'd simply pass in `VCons True $ VCons True $ VNil`,
what we're doing here is more akin to passing in an _execution trace_, i.e.
the execution of the "type family" is included in the program, and the type checker checks it.
### Doing existential quantification through universal quantification
Existential quantification can be expressed as universal quantification instead.
```haskell
newtype Some f = Some { runSome :: forall r. (forall a. f a > r) > r }
some :: f a > Some f
some x = Some $ \r > r x
```
Then we can instead define the above as:
```haskell
data VUCons' n a n' = VUCons' ('Succ n' :~: n) a (VecU n' a)
data VecU (n :: Nat) (a :: Type)
= VUNil (n :~: 'Zero)
 VUCons (Some (VUCons' n a))
data PlusUSucc' x y k x' = PlusUSucc' ('Succ x' :~: x) (PlusU x' ('Succ y) k)
data PlusU (x :: Nat) (y :: Nat) (k :: Nat > Type)
= PlusUZero (x :~: 'Zero) (k y)
 PlusUSucc (Some (PlusUSucc' x y k))
twoBoolsU :: PlusU ('Succ 'Zero) ('Succ 'Zero) (Flip VecU Bool)
twoBoolsU = PlusUSucc $ some $ PlusUSucc' refl $
PlusUZero refl $ Flip $ VUCons $ some $ VUCons' refl True $
VUCons $ some $ VUCons' refl True $ VUNil refl
```
## Can we go further?
The answer is yes. I assume you are familiar with the SKI calculus, if not,
it essentially works the following way:
```haskell
s :: (a > b > c) > (a > b) > a > c
s = (<*>)
k :: a > b > a
k = pure
i :: a > a
i = id
```
Using these three primitives, we can write any LC term
(with the same restrictions wrt. the type system used).
How can we leverage this here? We can use the CPS trick above
to define `newtype`s for the above constructs.
You could also define the AST as an ADT and then have the interpreter
be another ADT (using the Leibniz or GADT trick), but this seems simpler:
```haskell
type CPS a = (a > Type) > Type
infixr 0 ~>
type a ~> b = a > CPS b
type UnCPS' :: a > (b > Type) > (a ~> b) > Type
newtype UnCPS' x k f = UnCPS' (f x k)
type UnCPS :: CPS (a ~> b) > a ~> b
newtype UnCPS x y k = UnCPS (x (UnCPS' y k))
type S2' :: CPS (b ~> c) > (c > Type) > b > Type
newtype S2' f k x = S2' (UnCPS f x k)
type S2 :: (a ~> b ~> c) > (a ~> b) > a ~> c
newtype S2 f g x k = S2 (g x (S2' (f x) k))
type S1 :: (a ~> b ~> c) > (a ~> b) ~> a ~> c
newtype S1 f g k = S1 (k (S2 f g))
type S :: (a ~> b ~> c) ~> (a ~> b) ~> a ~> c
newtype S f k = S (k (S1 f))
type (<*>) a b = S :@ a :@ b
infixl 4 <*>
type K1 :: a > b ~> a
newtype K1 x y k = K1 (k x)
type K :: a ~> b ~> a
newtype K x k = K (k (K1 x))
type I :: a ~> a
newtype I x k = I (k x)
infixl 9 :@
type (:@) :: (a ~> c ~> d) > a > c ~> d
newtype (:@) x y z k = App (UnCPS (x y) z k)
```
We use the same CPS trick as used for turning type families into data families,
and thus are able to construct the following:
```hs
type S :: (a ~> b ~> c) ~> (a ~> b) ~> a ~> c
type K :: a ~> b ~> a
type I :: a ~> a
```
where `a ~> b` represents a typelevel computation using CPS,
i.e. it's defined as `a > (b > Type) > Type`.
Using the new application operator, `:@`, we can now move our
point~~free~~less programming to the typelevel!
```haskell
type FlipS :: (a ~> b ~> c) ~> b ~> a ~> c
type FlipS = S :@ (S :@ (K :@ S) :@ (S :@ (K :@ K) :@ S)) :@ (K :@ K)
type ComposeS :: (b ~> c) ~> (a ~> b) ~> a ~> c
type ComposeS = S :@ (K :@ S) :@ K
type (.) a b = ComposeS :@ a :@ b
infixr 8 .
type TwiceS :: a ~> (a ~> a ~> b) ~> b
type TwiceS = S :@ (S :@ (K :@ S) :@ (S :@ (K :@ (S :@ I)) :@ K)) :@ K
```
What does this gain us? Essentially, typelevel lambdas _without builtin language support_.
Quite powerful I'd say.
Can we then possibly go a step further? Could we, replace data kinds, with
SKIScottencoded versions?
The answer is very unfortunately "no" in Haskell, because _universal quantification isn't erased_ at the typelevel.
The issue:
```haskell
 In fact Churchencoded, but point stands.
type NatS :: Type
type NatS = forall a. a ~> (a ~> a) ~> a
type ZeroS :: NatS
type ZeroS = K
 Fails horribly!
{
/my/file:some:place: error:
• Couldn't match kind ‘a0 > CPS ((b0 ~> c0) ~> b0)’ with ‘Nat’
Expected kind ‘Nat ~> Nat’,
but ‘ComposeS :@ (S :@ I)’ has kind ‘(a0 ~> ((b0 ~> c0) ~> b0))
> ((a0 ~> ((b0 ~> c0) ~> c0)) > Type) > Type’
• In the type ‘ComposeS :@ (S :@ I)’
In the type declaration for ‘SuccS’

79  type SuccS = ComposeS :@ (S :@ I)
}
 type SuccS :: NatS ~> NatS
 type SuccS = ComposeS :@ (S :@ I)
```
Though `NatS` uses a `forall`, the `forall` doesn't work as expected.
The issue becomes more clear if we reformulate it into
```hs
type SI :: forall b. ((b ~> b) ~> b) ~> (b ~> b) ~> b
type SI = S :@ I
{
/my/file:some:place: error:
• Couldn't match kind: a0 > CPS ((b0 ~> b0) ~> b0)
with: forall a. a ~> ((a ~> a) ~> a)
Expected kind ‘(forall a. a ~> ((a ~> a) ~> a))
~> (forall b. b ~> ((b ~> b) ~> b))’,
but ‘ComposeS :@ SI’ has kind ‘(a0 ~> ((b0 ~> b0) ~> b0))
> ((a0 ~> ((b0 ~> b0) ~> b0)) > Type) > Type’
• In the type ‘ComposeS :@ SI’
In the type declaration for ‘SuccS’

78  type SuccS = ComposeS :@ SI
 ^^^^^^^^^^^^^^
}
type SuccS :: (forall a. a ~> (a ~> a) ~> a) ~> (forall b. b ~> (b ~> b) ~> b)
type SuccS = ComposeS :@ SI
```
If we take the crux of the error, it says it can't do the following
```hs
a0 ~> (b0 ~> b0) ~> b0
~
forall a. a ~> (a ~> a) ~> a
```
Both typings _would_ be valid for the above typelevel term,
_if_ the `forall` had been erased. Because it isn't, and is more
akin to an implicit function, GHC can't do anything, since we don't
have real typelevel lambdas, and the point is to avoid typelevel lambdas.
Though we have been defeated here, we can still have some fun,
albeit I've gone back to using real GADTs to help with type (term?) inference:
```haskell
data VecImpl (n :: Nat) (a :: Type) where
VImplNil :: VecImpl 'Zero a
VImplCons :: a > VecImpl n a > VecImpl ('Succ n) a
 Representation is equal to lists so we steal the instance
instance Show a => Show (VecImpl n a) where
showsPrec = unsafeCoerce $ showsPrec @[a]
show = unsafeCoerce $ show @[a]
showList = unsafeCoerce $ showList @[a]
type VecS1 :: Nat > Type ~> Type
newtype VecS1 (n :: Nat) (a :: Type) (k :: Type > Type)
= VecS1 (k (VecImpl n a))
type VecS :: Nat ~> Type ~> Type
newtype VecS (n :: Nat) (k :: (Type ~> Type) > Type)
= VecS (k (VecS1 n))
type PlusImpl :: Nat > Nat ~> Nat
data PlusImpl (x :: Nat) (y :: Nat) (k :: Nat > Type) where
PlusImplZero :: (k y) > PlusImpl 'Zero y k
PlusImplSucc :: PlusImpl x ('Succ y) k > PlusImpl ('Succ x) y k
type PlusS :: Nat ~> Nat ~> Nat
newtype PlusS x k = PlusS (k (PlusImpl x))
 We use SKI stuff to flip stuff around rather than simply using Flip as before
twoBoolsS ::
(FlipS :@ VecS :@ Bool . PlusS :@ 'Succ 'Zero)
('Succ 'Zero)
Identity
```
`twoBoolsS` is what you expect it to be, however, how do we define it?
The answer is that we ask GHC to infer it for us. Insert a typed hole, i.e. `twoBoolsS = _`, and let GHC guide you forward. Because _only one constructor_
is valid, GHC will essentially infer the term for you. When you reach
the case of `PlusImpl`, you need to try both, and one of them will make GHC err
because it's invalid.
What does the end result look like?
```haskell
twoBoolsS = App
$ UnCPS $ App $ UnCPS $ App $ UnCPS $ App $ UnCPS $ S $ UnCPS' $ S1
$ UnCPS' $ S2 $ K $ S2' $ UnCPS $ App $ UnCPS $ K $ UnCPS' $ K1 $ UnCPS'
$ S $ UnCPS' $ S1 $ UnCPS' $ S2 $ App $ UnCPS $ PlusS $ UnCPS' $ PlusImplSucc
$ PlusImplZero $ S2' $ UnCPS $ K1 $ UnCPS' $ App $ UnCPS $ App $ UnCPS
$ App $ UnCPS $ App $ UnCPS $ S $ UnCPS' $ S1 $ UnCPS' $ S2 $ App $ UnCPS
$ K $ UnCPS' $ K1 $ S2' $ UnCPS $ App $ UnCPS $ App $ UnCPS $ S $ UnCPS'
$ S1 $ UnCPS' $ S2 $ App $ UnCPS $ App $ UnCPS $ S $ UnCPS' $ S1 $ UnCPS'
$ S2 $ S $ S2' $ UnCPS $ App $ UnCPS $ K $ UnCPS' $ K1 $ UnCPS' $ K $ S2'
$ UnCPS $ App $ UnCPS $ K $ UnCPS' $ K1 $ UnCPS' $ S $ UnCPS' $ S1 $ UnCPS'
$ S2 $ K $ S2' $ UnCPS $ K1 $ UnCPS' $ S1 $ UnCPS' $ S2 $ K1 $ S2' $ UnCPS
$ VecS $ UnCPS' $ VecS1 $ Identity $ VImplCons True $ VImplCons False $ VImplNil
```
No one said this would be pr\*tty.
It took me a painstaking amount of time to do the above with GHCi.
I assume it would be faster if you used HLS. You could
theoretically also completely automate it upto the uninferrable parts, i.e.
the two booleans you choose (`True` and `False` in my case).
## Conclusion
Maybe the above wasn't a good idea after all.
Maybe there was a reason they added type families (surprisingly).
I would (unironically) however recommend using
data families instead wherever possible as they are much easier to infer
types for (given that they _are_ normal data types mostly).
I'm especially annoyed by the fact that many people create associated
type families that end in `> Type`, yet don't use a data family.
You have absolutely no good reason most of the time!
There is one notable realworld use case however:
Given any complex data type, you can apply the above transformations to
turn it into something that you can derive `Generic` for,
if you also turn any instance of universal quantification into
explicit uses of a `Forall` type.
You can also handle recursive types by turning recursion into using
explicit fixpoints using `Fix`.
## Aside: Handling type family overlapping instances (for matching types)
Given this:
```haskell
type family IsUnit (x :: Type) :: Bool where
IsUnit () = 'True
IsUnit _ = 'False
```
How do we use the above tricks?
Converting it into a data family doesn't work:
```hs
data family IsUnitD (a :: Type) (k :: Bool > Type)
newtype instance IsUnitD () k = IsUnitDY (k 'True)
newtype instance IsUnitD _ k = IsUnitDN (k 'False)
```
If all you want to do is improve inference, do the following instead:
```haskell
newtype IsUnitD (a :: Type) (k :: Bool > Type) = IsUnitD (k (IsUnit a))
```
If however you want to see how to replicate this in languages with fewer features,
you could naively do:
```haskell
data IsUnitG (a :: Type) (k :: Bool > Type) where
IsUnitGY :: (k 'True) > IsUnitG () k
IsUnitGN :: (k 'False) > IsUnitG a k
```
The issue is this is wrong! In the case of `()`, both constructors
are valid. We need an _inequality proof_:
```haskell
data IsUnitE (a :: Type) (k :: Bool > Type)
= IsUnitEY (a :~: ()) (k 'True)
 IsUnitEN (a :~: () > Void) (k 'False)
data SBool (b :: Bool) where
STrue :: SBool 'True
SFalse :: SBool 'False
handleIsUnitEY :: IsUnitE () SBool > SBool 'True
handleIsUnitEY (IsUnitEY _ b) = b
handleIsUnitEY (IsUnitEN p _) = case p refl of
handleIsUnitEN :: IsUnitE Int SBool > SBool 'False
handleIsUnitEN (IsUnitEY _ _) = error "impossible"
handleIsUnitEN (IsUnitEN _ b) = b
```
This is one aspect where using explicit equalities is more
powerful than using data families and GADTs.
If only the above type could be a newtype!
However, there is an issue: It is not clear to me how you would construct
`a :~: b > Void` for two different types `a` and `b`
(i.e., the heads when in WHNF differ).
Take for example, `Int :~: ()`, which we get from the `IsUnitEY` case in
`handleIsUnitEN`: Can we somehow reduce this to `False :~: True` to make
use of the "trusted" function `absurd`? Naive solutions end up
with an open branch with `Int :~: ()` in scope again, thus resulting in a cycle,
unless you use type families etc., which ruins the point.
# About me
Type theorist.
Rolling my own crypto.
 Email: mdwuaidiuawhdiuhe`@`{=html};lajxujxujuxjujus.rs
 GitHub: [\@Las](https://github.com/Las)
 Matrix: [\@Las:matrix.org](https://matrix.to/#/@Las:matrix.org)
# Posts
 [All you need is higher kinded types](/blog/allyouneedishkts.html)  20230113
 [Using Haskell as my shell](/blog/haskellasshell.html)  20210723
 [vfork, close_range, and execve for launching processes in Procex](/blog/vfork_close_execve.html)  20210720
 [F2FS swap files broken and the arcane ritual to fix them](/blog/f2fs.html)  20210707
This page has a [markdown version](./allyouneedishkts.md)
[Atom Feed](/atom.xml)
[Public PGP key (6B66 1F36 59D3 BAE7 0561 862E EA8E 9467 5140 F7F4)](/publicpgpkey.txt)