Haskell implementation of normalization by evaluation

nbe.hs

{-# LANGUAGE GADTs, NoImplicitPrelude, StandaloneDeriving, RankNTypes #-}

module NBE where

import Data.Monoid
import Control.Category
import Prelude hiding ((.), id, fst, snd)
import Control.Arrow ((&&&))
data FM a = Pure a | Mappend (FM a) (FM a) | Mempty deriving (Eq, Show)

instance Semigroup (FM a) where
   (<>) = Mappend
instance Monoid (FM a) where
   mempty = Mempty


lift :: FM a -> (FM a -> FM a)
lift (Pure x) = \y -> (Pure x) <> y
lift (Mappend x y) = (lift x) . (lift y) 
lift Mempty = id

-- using Endo is kind of less clear
-- lift' :: FM a -> Endo (FM a)
-- lift' (Pure x) = Endo $ \y -> (Pure x) <> y
-- lift' (Mappend x y) = (lift' x) <> (lift' y) 
-- lift' Mempty = mempty

lift' :: Monoid b => (a -> b) -> (FM a -> b)
lift' f (Pure x) = f x
lift' f (Mappend x y) = (lift' f x) <> (lift' f y) 
lift' _ Mempty = mempty

lift'' = lift' Endo

normalize :: FM a -> FM a
normalize x = lift x Mempty

eq' :: Eq a => FM a -> FM a -> Bool
eq' x y = (normalize x) == (normalize y)


{-
This isn't quite a great replica of a monoid considered as a category
Instead of having a single object, it feels like we have the same objects as Hask
however only morphisms going from each object to itself
-}

data MonoidCat m a b where
   MonoidCat :: m -> MonoidCat m a a


deriving instance Eq m => Eq (MonoidCat m a b)
deriving instance Show m => Show (MonoidCat m a b)

instance Monoid m => Category (MonoidCat m) where
   id = MonoidCat mempty
   (MonoidCat x) . (MonoidCat y) = MonoidCat (x <> y)


data FreeCCC a b where
   Id :: FreeCCC a a
   Comp :: FreeCCC b c -> FreeCCC a b -> FreeCCC a c
   Fst :: FreeCCC (a,b) a
   Snd :: FreeCCC (a,b) b
   Fan :: FreeCCC a b -> FreeCCC a c -> FreeCCC a (b,c)
   -- Pure' :: k a b -> FreeCCC k a b
-- deriving instance (Eq a, Eq b) => Eq (FreeCCC a b)
deriving instance Show (FreeCCC a b)


  
{-
data FreeCCC k a b where
   Id :: FreeCCC k a a
   Comp :: FreeCCC k b c -> FreeCCC k a b -> FreeCCC k a c
   Fst :: FreeCCC k (a,b) a
   Snd :: FreeCCC k (a,b) b
   Fan :: FreeCCC k a b -> FreeCCC k a c -> FreeCCC k a (b,c)
   Pure' :: k a b -> FreeCCC k a b

analog of Endo?
newtype Yoneda :: forall b. (a -> b) -> f b
YonedaEmbed k = forall s. (k s a) -> (k s b)

instance Category k => Category (YonEm k) where
   id = id
   
instance Cartesian k => Cartesian (YonEmb k)

interpccc :: CCC k => (k a b -> k' a b) -> FreeCCC k a b -> (k' a b)
interpccc m Id = id
interpccc m (Comp f g) = (interpccc m f) . (interpccc m g)
interpccc 


interpccc :: (YonEmb Id) -> FreeCCC -> 




-}


instance Category FreeCCC where
   id = Id
   (.) = Comp

class Category k => CartesianCategory k where
   fst :: k (a,b) a 
   snd :: k (a,b) b
   fanin :: k a b -> k a c -> k a (b,c)

instance CartesianCategory FreeCCC where
   fst = Fst
   snd = Snd
   fanin = Fan

instance CartesianCategory (->) where
   fst (x,_) = x
   snd (_,y) = y
   fanin = (&&&)

data Ty f a where
   Tup :: Ty f a -> Ty f b -> Ty f (a,b)
   -- Arr :: (Tup f a -> Tup f b) -> Tup f (a -> b)
   PureTy :: f a -> Ty f a


par :: CartesianCategory k => k a b -> k c d -> k (a,c) (b,d)
par f g = fanin (f . fst) (g . snd)

dup :: CartesianCategory k => k a (a,a)
dup = fanin id id
 
interp :: FreeCCC a b -> Ty (FreeCCC s) a -> Ty (FreeCCC s) b
interp Id x = x
interp (Comp f g) x = (interp f) $ (interp g) $ x
interp Fst (Tup x y) = x
interp Fst (PureTy x) = PureTy $ Fst . x
interp Snd (Tup x y) = y
interp Snd (PureTy x) = PureTy $ Snd . x
interp (Fan f g) x = Tup (interp f x) (interp g x)
-- interp (Pure' k)

build :: (forall s. Ty (FreeCCC s) a -> Ty (FreeCCC s) b) -> FreeCCC a b
build f = flup r
   where 
   r = f (PureTy Id)
   flup :: Ty (FreeCCC a) b -> FreeCCC a b
   flup (Tup x y) = Fan (flup x) (flup y)
   flup (PureTy x) = x


normalizeCCC :: FreeCCC a b -> FreeCCC a b
normalizeCCC f = build (interp f)