Orbits.hs

{-# LANGUAGE DataKinds              #-}
{-# LANGUAGE PolyKinds              #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TypeApplications       #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE TypeInType             #-}
{-# LANGUAGE TypeOperators          #-}
{-# LANGUAGE UndecidableInstances   #-}
{-# OPTIONS_GHC -Wall                       #-}
{-# OPTIONS_GHC -Werror=incomplete-patterns #-}

{-|

Example on how to do compile-time (ie type-level) computations and how
to get the results into use on term-level (ie runtime).

The original problem is described in
[aoc 19 d6](https://adventofcode.com/2019/day/6). We use the described
example input data in a bit different form. See the link for the
original data and answer.

-}

--------------------------------------------------------------------------------

import qualified GHC.TypeLits as TL

import           Data.Proxy

import           Fcf
import           Fcf.Data.Nat
import           Fcf.Data.List as L

import           Fcf.Alg.Morphism
import           Fcf.Alg.List
import           Fcf.Alg.Tree

--------------------------------------------------------------------------------


-- | Type-level variable containing all the required information.
data OrbitInput :: Exp [(TL.Symbol, TL.Symbol)]
type instance Eval OrbitInput =
                   '[ '("COM", "B")
                    , '("B", "C")
                    , '("C", "D")
                    , '("D", "E")
                    , '("E", "F")
                    , '("B", "G")
                    , '("G", "H")
                    , '("D", "I")
                    , '("E", "J")
                    , '("J", "K")
                    , '("K", "L")]

-- helper, we might could do without this one
-- This is used to check that two symbols are same.
data EqPlanet :: TL.Symbol -> TL.Symbol -> Exp Bool
type instance Eval (EqPlanet a b) = Eval (TyEq 'EQ (TL.CmpSymbol a b))

-- | :kind! Eval (FindDescs "COM" =<< OrbitInput)
data FindDescs :: TL.Symbol -> [(TL.Symbol, TL.Symbol)] -> Exp [TL.Symbol]
type instance Eval (FindDescs p lst) = 
    Eval (Map Snd =<< (Filter (EqPlanet p <=< Fst) lst))

-- | This is not used in the final solution but worked as a step towards it.
--
-- :kind! Eval (Ana BuildOrbTreeCoA "COM")
data BuildOrbTreeCoA :: CoAlgebra (TreeF TL.Symbol) TL.Symbol
type instance Eval (BuildOrbTreeCoA nd) =
    If (Eval (L.Null (Eval (FindDescs nd =<< OrbitInput))))
        ('NodeF nd '[])
        ('NodeF nd (Eval (FindDescs nd =<< OrbitInput)))

-- |
-- We need to store the depth of the node along the tree. We use the depth when
-- counting paths from root to every node.
--
-- :kind! Eval (Ana BuildOrbTreeCoA2 '(0,"COM"))
data BuildOrbTreeCoA2 :: CoAlgebra (TreeF (Nat,TL.Symbol)) (Nat,TL.Symbol)
type instance Eval (BuildOrbTreeCoA2 '(d,nd)) =
    If (Eval (L.Null (Eval (FindDescs nd =<< OrbitInput))))
        ('NodeF '(d,nd) '[])
        ('NodeF '(d,nd) (Eval (MkPairLst (1 TL.+ d) =<< FindDescs nd =<< OrbitInput)))

-- helper, we might could do without this one
data MkPair :: Nat -> TL.Symbol -> Exp (Nat,TL.Symbol)
type instance Eval (MkPair n s) = '(n,s)

-- helper, we might could do without this one
data MkPairLst :: Nat -> [TL.Symbol] -> Exp [(Nat,TL.Symbol)]
type instance Eval (MkPairLst n lst) = Eval (Map (MkPair n) lst)


-- | Count paths from root to every node.
--
-- If it is a leaf, the number of paths from root to it is the depth.
-- If it is an internal node, the number of paths to the subtree rooted
-- by it is sum of pathnums of subtrees plus the depth (paths to this one).
data CountPathsAlg :: Algebra (TreeF (Nat,TL.Symbol)) Nat
type instance Eval (CountPathsAlg ('NodeF '(d,_) '[])) = d
type instance Eval (CountPathsAlg ('NodeF '(d,_) (b ': bs))) = d TL.+ (Eval (Sum (b ': bs)))


-- | We initialize this with the known starting node and the depth of it, which
-- is 0.
--
-- :kind! Eval OrbitSolution
data OrbitSolution :: Exp Nat
type instance Eval OrbitSolution =
    Eval (Hylo CountPathsAlg BuildOrbTreeCoA2 '(0,"COM"))

-- | Helper to bring in the result of the type-level computation.
--
-- It is a nice exercise to solve this using Tree, UnfoldTree and FoldTree.
showResult :: forall n. (n ~ Eval OrbitSolution) => String
showResult = show $ TL.natVal @n Proxy

main :: IO ()
main = putStrLn $ "Number of orbits is " ++ showResult