{-# OPTIONS_GHC -freduction-depth=1000 #-} 
{-# LANGUAGE 
     FlexibleContexts, FlexibleInstances, FunctionalDependencies, 
     MultiParamTypeClasses, TypeSynonymInstances, 
     TypeOperators, UndecidableInstances, TypeFamilies #-} 
module T5321FD where

-------- USES FUNCTIONAL DEPENDENCIES -------------

-- Our running example, for simplicity's sake, is a type-level map of a
-- single function. For reference, here is the code for a simple
-- value-level map of a single function.

-- vfoo = id
-- mapfoo (x : xs) = vfoo x : mapfoo xs
-- mapfoo [] = []

-- Because Haskell is a lazy language, this runs in O(n) time and constant stack.

-- We now lift map to the type level, to operate over HLists.

-- First, the basic HList types

infixr 3 :*
data x :* xs = x :* xs deriving Show
data HNil = HNil deriving Show

-- Next, a large boring HList

-- Adds ten cells
addData x = i :* i :* d :* d :* s :* 
            i :* i :* d :* d :* s :* 
            x 
    where i = 1 :: Int 
          d = 1 :: Double 
          s = "" 

-- Has 70 cells. 
sampleData = addData $ addData $ addData $ addData $ addData $ 
             addData $ addData $ 
             HNil

-- Next, a simple polymorphic function to map

class Foo x y | x -> y 
    where foo :: x -> y 
          foo = undefined

instance Foo Int Double
instance Foo Double Int
instance Foo String String

------------------------
-- Now, our map

class HMapFoo1 as bs | as -> bs where 
    hMapFoo1 :: as -> bs

instance (Foo a b, HMapFoo1 as bs) => HMapFoo1 (a :* as) (b :* bs) where 
    hMapFoo1 (x :* xs) = foo x :* hMapFoo1 xs

instance HMapFoo1 HNil HNil where 
    hMapFoo1 _ = HNil

-- If we enable the following line, compilation time is ~ 9 seconds.

testHMapFoo1 = hMapFoo1 sampleData 


------------------------
class HMapFoo2 acc as bs | acc as -> bs where 
    hMapFoo2 :: acc -> as -> bs

instance (Foo a b, HMapFoo2 (b :* bs) as res) => HMapFoo2 bs (a :* as) res where 
    hMapFoo2 acc (x :* xs) = hMapFoo2 (foo x :* acc) xs

instance HMapFoo2 acc HNil acc where 
    hMapFoo2 acc _ = acc

-- If we enable the following line, compilation time is a much more satisfying ~0.5s.

testHMapFoo2 = hMapFoo2 HNil sampleData 

------------------------
-- But wait, there's trouble on the horizon! Consider the following version: 

class HMapFoo3 acc as bs | acc as -> bs where 
    hMapFoo3 :: acc -> as -> bs

instance (HMapFoo3 (b :* bs) as res, Foo a b) => HMapFoo3 bs (a :* as) res where 
    hMapFoo3 acc (x :* xs) = hMapFoo3 (foo x :* acc) xs

instance HMapFoo3 acc HNil acc where 
    hMapFoo3 acc _ = acc

-- The only difference between hMapFoo2 and hMapFoo3 is that the order of
-- constraints on the inductive case has been reversed, with the
-- recursive constraint first and the immediately checkable constraint
-- second. Now, if we enable the following line, compilation time rockets
-- to ~6s!

testHMapFoo3 = hMapFoo3 HNil sampleData