Pair using Datatype

pair.hs

{-# Language MultiParamTypeClasses,UndecidableInstances,AllowAmbiguousTypes,ScopedTypeVariables,RankNTypes,TypeApplications,PolyKinds,DataKinds,TypeFamilies,GADTs,TypeOperators #-}

import Data.Proxy
import Data.Kind
import GHC.Types (Symbol)

----
-- To

type family To k o (a :: k) :: o

class Has a b where
 to :: a -> b

----
-- Container

type Container = * -> *

type H_Container container k = container k -> *

type F_Container (container :: Container) k l = (k -> l) -> container k -> *

--type FN_Container (container :: Container) k a xs = FunctionList a xs k -> container k -> *

-- casting H & F _Container to Container

type instance To (H_Container container k) Container hContainer = container

type instance To (F_Container container k l) Container fContainer = container

-- casting between H & F _Container's

type instance To (H_Container container k) (F_Container container k l) hcontainer 
 = To Container (F_Container container k l) (To (H_Container container k) Container hcontainer)

type instance To (F_Container container k l) (H_Container container k) fcontainer 
 = To Container (H_Container container k) (To (F_Container container k l) Container fcontainer)

----
-- List

data HList (xs :: [k]) where
 HEmpty :: HList '[]
 HCons  :: x -> HList xs -> HList (x ': xs)

data FList (f :: k -> l) (xs :: [k]) where
 FEmpty :: FList f '[]
 FCons  :: f x -> FList f xs -> FList f (x ': xs)

toFList :: forall (f :: * -> *) (xs :: [*]). (forall (a :: *). a -> f a) -> HList xs -> FList f xs
toFList f HEmpty = FEmpty 
toFList f (HCons x xs) = FCons (f x) $ toFList f xs

type instance To Container (H_Container [] k) [] = HList 

type instance To Container (F_Container [] k l) [] = FList 

----
-- Sum

data Sum_T k = Sum_T Symbol [(Symbol,k)]

type family Lookup (i :: a) (xs :: [ (a,b)]) :: b where
 Lookup i ( '(i,b) ':xs) = b
 Lookup i ( '(a,b) ':xs) = Lookup i xs

data Sum (xs :: Sum_T k) where 
 Sum :: Proxy (name :: Symbol) -> Lookup name nts -> Sum ('Sum_T name nts)

toSum :: forall name nts. Lookup name nts -> Sum ('Sum_T name nts)
toSum = Sum Proxy

fromSum :: 
  forall name (name' :: Symbol) nts.
  Sum ('Sum_T name nts) -> Lookup name nts
fromSum (Sum _ x) = x

type Unit_T name a = 'Sum_T name '[ '(name,a)]
type Unit a = Sum (Unit_T "unit" a)

toUnit :: a -> Unit a
toUnit = toSum 

testUnit :: Int
testUnit = fromSum $ toUnit 1

-- strips the f off the input args type and stores it as xs
data FSum (f :: k -> *) (xs :: Sum_T k) where
 FSum :: Proxy (name :: Symbol) -> f (Lookup name nts) -> FSum f ('Sum_T name nts)

toFSum :: forall f name nts. f (Lookup name nts) -> FSum f ('Sum_T name nts)
toFSum = FSum Proxy

fromFSum :: 
  forall f name (name' :: Symbol) nts.
  FSum f ('Sum_T name nts) -> f (Lookup name nts)
fromFSum (FSum _ x) = x

type FUnit name f a = FSum f (Unit_T name a)

toFUnit :: f a -> FUnit name f a
toFUnit = toFSum 

type instance To Container (H_Container Sum_T k) Sum_T = Sum 

type instance To Container (F_Container Sum_T k *) Sum_T = FSum 

----
-- Free and Free'

data Free f a where
 Free :: (f (Free f a)) -> Free f a 
 Pure :: a -> Free f a 

data Free' f a where
 Free' :: (f (Free f a)) -> Free' f a
 Pure' :: f a -> Free' f a 

-- HFree wraps the result of unmapping the HFree constructor from the HFrees passed as an argument.
data HFree (k :: z) where
 HFree :: (fList :: (k -> *) -> container k -> *) HFree xs    
       -> HFree ((To (F_Container container k *) 
                     (H_Container container k) fList) xs)
 HPure :: (x :: *) -> HFree x

-- if we dont want to allow for this verticle hetrogeneity,
-- we can use;

data HFree' (container :: * -> *) (k :: z) where
 HFree' :: (fList :: (k -> *) -> container k -> *) (HFree' container) xs    
       -> HFree' container ((To (F_Container container k *) 
                            (H_Container container k) fList) xs)
 HPure' :: (x :: *) -> HFree' container x

type HTree = HFree' []

type SumTree = HFree' Sum_T

----
-- Datatype

data Datatype_Layer_T a = Datatype_Layer_T (Sum_T [a])

data Datatype_Layer (xs :: Datatype_Layer_T a) where
 Datatype_Layer :: FSum HList (xs :: (Sum_T [a])) -> Datatype_Layer ('Datatype_Layer_T xs)

data FDatatype_Layer (f :: k -> l) (xs :: Datatype_Layer_T k) where
 FDatatype_Layer :: FSum (FList f) xs -> FDatatype_Layer f ('Datatype_Layer_T xs)

type instance To Container (H_Container Datatype_Layer_T k) Datatype_Layer_T = Datatype_Layer 

type instance To Container (F_Container Datatype_Layer_T k *) Datatype_Layer_T = FDatatype_Layer 

type Datatype = HFree' Datatype_Layer_T 

----
-- Product f

type Product_T name (xs :: [a]) = FUnit name HList xs

toProduct_T :: HList xs -> Product_T name xs
toProduct_T = toFUnit

type Product_Layer name xs = Datatype_Layer ('Datatype_Layer_T (Unit_T name xs))

type FProduct_Layer f name xs = FDatatype_Layer f ('Datatype_Layer_T (Unit_T name xs))

type Product name xs = Datatype (Product_Layer name xs)

----
-- Pair

type Pair_T a b = Product_T "pair" '[a,b]
--              = FUnit name HList '[a,b]          -- via; type Product name (xs :: [a]) = FUnit name HList xs
--              = FSum HList (Unit_T name '[a,b])  -- via; type FUnit name f a = FSum f (Unit_T name a)
--              = FSum HList ('Sum_T name '[ '(name, '[a,b])]) -- via; type Unit_T name a = 'Sum_T name '[ '(name,a)]

toHPair :: (a,b) -> HList '[a,b]
toHPair (a,b)  = a `HCons` (b `HCons` HEmpty)

type Pair_Layer a b = Product_Layer "pair" '[a, b]

type FPair_Layer a b = FProduct_Layer Datatype "pair" '[a, b]

toPairLayer' :: (a,b) -> FPair_Layer a b
toPairLayer'  = FDatatype_Layer . toFUnit . toFList HPure' . toHPair 

type Pair a b = Datatype (Pair_Layer a b)

toPair :: (a, b) -> Pair a b 
toPair = HFree' . toPairLayer'