Build.hs

{-# OPTIONS_HADDOCK not-home #-}

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE InstanceSigs           #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}

{-|
Module      : HList.Build
Description : Build an HList with a specialised function.
Copyright   : (c) Tom Harding, 2018
License     : MIT
Maintainer  : tom.harding@habito.com
Stability   : experimental

The construction of an HList can be quite tedious because there's no special
syntax (and we can't use OverloadedLists because it's homogeneous). To make it
a bit neater, this module provides a `build` function, which produces a
parameter for each element of the HList.

>>> :{
f :: HList '[]
f = build
:}

>>> :{
g :: Int -> HList '[Int]
g = build
:}

>>> :{
h :: String -> Int -> HList '[String, Int]
h = build
:}

This pattern generalises to any number of parameters, and inference seems to be
pretty good. The one gotcha is that you'll see plenty of internals if you try
to ask for the type of a call to 'build' without annotating the eventual
@HList@ anywhere.

>>> :t build 2 "hello" True
build 2 "hello" True
  :: (BuildLoop tail (t : [Char] : Bool : tail), Num t) =>
     Signature tail (t : [Char] : Bool : tail)

This is unfortunate, but makes sense: is @build 2@ an @HList '[Int]@, or is it
@String -> HList '[Int, String]@? For any call to build, there are a literally
infinite number of possible interpretations, so it's worth specifying the HList
you actually want to build (as above).
-}
module HList.Build where

import Data.Kind    (Type)
import HList.Types  (HList (..))
import Prelude      hiding (head)

-- | This type family takes a list of types and an outupt type, and rolls it
-- out into a function. Originally, it was called @Uncurry@, and the result
-- wasn't necessarily an HList. However, I ran into (what I think is) a pretty
-- fun problem.
--
-- The type of 'build' was /always/ ambiguous. I needed to type-apply the
-- entire list of types to get it to behave, which is obviously not the nicest
-- developer experience. At the time, the signature of 'build' was @Uncurry
-- list (HList list)@, which would expand depending on list. However, it wasn't
-- injective. In other words, you couldn't figure out the inputs if you knew
-- the outputs. For example:
--
-- @
--    Uncurry '[a, b] c     == a -> b -> c
--    Uncurry '[a] (b -> c) == a -> b -> c
-- @
--
-- What this meant was that, if I annotated a call to 'build' with @Int ->
-- HList '[Int]@, that wasn't enough information to figure out what the inputs
-- would be, so it would complain about ambiguity until I made it explicit.
--
-- Enter @TypeFamilyDependencies@. If our result is always an 'HList', we /can/
-- always know the inputs. In fact, with this extension, we can even make it
-- explicit with something that looks an awful lot like a functional
-- dependency. Now inference works, and I learnt a new thing!
type family Signature (list :: [Type]) (output :: [Type]) = (done :: Type)
    | done -> list output where
  Signature '[]            original = HList original
  Signature (head ': tail) original = head -> Signature tail original

-- | There's an interesting problem to be solved here: our arguments for this
-- function are the reverse to what would be easiest (we can't just @HCons@
-- them on!). A naïve implementation would take each parameter, put it into
-- an @\x -> HCons x HNil@ singleton, and then concat them all together. We
-- can do slightly better, however, with a DList:
--
-- @
--   type DList a = [a] -> [a]
-- @
--
-- It's definitely an unintuitive type, but the summary is: instead of all
-- the appends, we build a function of /prepends/. When we want to append
-- something, we pre-compose it with our current function, and then it goes
-- first. As all the functions are just 'HCons', we get exactly what we want!
-- Even better: it's O(1) to add each element!
class BuildLoop (todo :: [Type]) (original :: [Type]) where

  buildLoop :: (HList todo -> HList original) -> Signature todo original


instance BuildLoop '[] original where

  -- | We have none left "to do", so we can just pass in an empty @HList@ and
  -- set off the composition chain. The result of this will be our list!
  buildLoop :: (HList '[] -> HList original) -> HList original
  buildLoop diff = diff HNil


instance BuildLoop tail original => BuildLoop (head ': tail) original where

  -- | Here, we have a DList that requires a @head@ type from us. So, we ask
  -- for that as a parameter, and then pre-compose a function to our DList that
  -- will 'HCons' it on. This hurts my head if I think about it too much, but
  -- we're really just saying "each step of this recursion should produce a
  -- parameter /before/ the last", rather than after. It's neat.
  buildLoop
    :: (HList (head ': tail) -> HList original)
    -> head
    -> Signature tail original

  buildLoop diff head
    = buildLoop @tail (diff . (HCons head))


-- | This is the class (and function) that users will actually see, and all
-- it does  is pass through to 'buildLoop'. However, it does so with a fully
-- injective type signature (i.e. one whose output is unique for each input),
-- so GHC can work backwards to figure out our parameters without type
-- application. GHC is way cleverer than we admit.
class Build original where

  build :: Signature original original


instance BuildLoop original original => Build original where

  -- | Our instance is straightforward: we can deduce the type of the output
  -- loop based on the call site for this function, but we can't necessarily
  -- deduce what's left "to do". However, we know that the 'build' function is
  -- called when /everything/ is left to do, so we can type-apply @original@ to
  -- the @todo@ list in @BuildLoop@ and everything works!
  build = buildLoop @original id