Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- {-# LANGUAGE
- RankNTypes,
- TypeApplications,
- TypeOperators,
- KindSignatures,
- TypeFamilies,
- TypeInType,
- MultiParamTypeClasses,
- FunctionalDependencies,
- FlexibleInstances,
- AllowAmbiguousTypes #-}
- module Test where
- import Prelude hiding (Monoid)
- import qualified Prelude as P
- import Data.Proxy
- import Control.Applicative
- import Data.Functor.Compose
- import Data.Functor.Identity
- import Control.Monad
- class Set p k | p -> k where
- class Set p k => Category p k | p -> k where
- type (→) :: k -> k -> *
- infixl 1 →
- data (a ≅ b) p = Iso { fwd :: a `p` b, bwd :: b `p` a }
- infixl 1 ≅
- class Category p k => Monoidal p k | p -> k where
- type (⊗) :: k -> k -> k
- type I :: k
- α :: forall (a :: k) (b :: k) (c :: k). ((a ⊗ b) ⊗ c ≅ a ⊗ (b ⊗ c)) (→)
- λ :: forall (a :: k) . (I ⊗ a ≅ a) (→)
- ρ :: forall (a :: k) . (a ⊗ I ≅ a) (→)
- class (Monoidal p c, Monoidal q d) => MonoidalFunctor p q (f :: c -> d) where
- ϕ :: (f a ⊗ f b) → f (a ⊗ b)
- ϕI :: I → f I
- class (Monoidal p c, Monoidal q d) => OpMonoidalFunctor p q (f :: c -> d) where
- ϕ' :: f (a ⊗ b) → (f a ⊗ f b)
- ϕI' :: f I → I
- class Monoidal p k => Monoid p (m :: k) where
- μ :: m ⊗ m → m
- η :: I → m
- data Hask
- instance Set Hask *
- instance Category Hask * where
- type (→) = (->)
- instance Monoidal Hask * where
- type (⊗) = (,)
- type I = ()
- α = Iso fwd bwd
- where
- fwd ((a, b), c) = (a, (b, c))
- bwd (a, (b, c)) = ((a, b), c)
- ρ = Iso fwd bwd
- where
- fwd (a, _) = a
- bwd a = (a, ())
- λ = Iso fwd bwd
- where
- fwd (_, a) = a
- bwd a = ((), a)
- instance Applicative f => MonoidalFunctor Hask Hask f where
- ϕ = uncurry $ liftA2 (,)
- ϕI = pure
- instance P.Monoid m => Monoid Hask m where
- μ = uncurry (<>)
- η _ = mempty
- data Hask'
- newtype f :~> g = Nat { runNat :: forall x. f x -> g x }
- newtype (f :&: g) a = Product { runProduct :: (f a, g a) }
- -- instance Set Hask' (* -> *)
- --
- -- instance Category Hask' (* -> *) where
- -- type (→) = (:~>)
- -- instance Monoidal Hask' (* -> *) where
- -- type (⊗) = (:&:)
- -- type I = (Const ())
- -- instance Alternative f => Monoid Hask' f where
- -- μ = Nat $ uncurry (<|>) . runProduct
- -- η = Nat $ const empty
- type f ∘ g = Compose f g
- data HaskC
- instance Set HaskC (* -> *)
- instance Category HaskC (* -> *) where
- type (→) = (:~>)
- instance Monoidal HaskC (* -> *) where
- type (⊗) = Compose
- type I = Identity
- α = Iso fwd bwd
- where
- -- fwd :: ((f ∘ g) ∘ h) :~> (f ∘ (g ∘ h))
- fwd = Nat $ _ . getCompose . getCompose
- -- bwd :: (f ∘ (g ∘ h)) :~> ((f ∘ g) ∘ h)
- bwd = Nat $ _
- ρ = Iso fwd bwd
- where
- -- fwd :: (f ∘ Identity) :~> f
- fwd = Nat $ _
- -- bwd :: f :~> (f ∘ Identity)
- bwd = Nat $ _
- λ = Iso fwd bwd
- where
- -- fwd :: (Identity ∘ f) :~> f
- fwd = Nat $ _
- -- bwd :: f :~> (Identity ∘ f)
- bwd = Nat $ _
- instance Monad m => Monoid HaskC m where
- μ = Nat $ join . getCompose
- η = Nat $ return . runIdentity
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement