{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# OPTIONS_GHC -Wall #-}
--------------------------------------------------------------------
-- |
-- Copyright :  (c) Edward Kmett 2014
-- License   :  BSD3
-- Maintainer:  Edward Kmett <ekmett@gmail.com>
-- Stability :  experimental
-- Portability: non-portable
--
--------------------------------------------------------------------
module Hask.Constrained where

import Hask.Core
import Hask.Rep

infixr |=

-- |
-- @(|=) :: Constraint -> * -> *@
--
-- This is a corepresentable profunctor
newtype p |= q = Constrained { runConstrained :: p => q }

instance Contravariant (|=) where
  contramap ab = Nat $ \bc -> Constrained $ case ab of
    Sub Dict -> runConstrained bc

instance Functor ((|=) e) where
  fmap bc ab = Constrained $ bc (runConstrained ab)

instance Semimonoidal ((|=) e) where
  ap2 (ea,eb) = Constrained $ (runConstrained ea, runConstrained eb)

instance Monoidal ((|=) e) where
  ap0 () = Constrained ()

instance Semimonad ((|=) e) where
  join cc = Constrained (runConstrained (runConstrained cc))

instance Semigroup p => Semigroup (e |= p) where
  mult = multM

instance Monoid p => Monoid (e |= p) where
  one = oneM

instance Cosemimonad ((|=) e) where
  duplicate cc = Constrained cc

instance Monoid e => Comonad ((|=) e) where
  extract cc = runConstrained cc \\ (one :: () :- e)

instance Corepresentable (|=) where
  type Corep (|=) = Dict
  _Corep = dimap (\ab Dict -> case ab of Constrained b -> b) (\ab -> Constrained $ ab Dict)

-- | We could flip this around to permit a @Curried@ instance, but then we lose a lot of structure.
data EnvC p q = EnvC (Dict p) q

-- EnvC p (Either a b) -> Either (EnvC p a) (EnvC p b)

instance Functor EnvC where
  fmap f = Nat $ \(EnvC p q) -> EnvC (fmap f p) q

instance Functor (EnvC p) where
  fmap f (EnvC p q) = EnvC p (f q)

instance Cosemimonad (EnvC p) where
  duplicate q@(EnvC p _) = EnvC p q

instance Comonad (EnvC p) where
  extract (EnvC _ q) = q

instance Cosemimonoidal (EnvC p) where
  op2 (EnvC p eab) = bimap (EnvC p) (EnvC p) eab

instance Comonoidal (EnvC p) where
  op0 (EnvC _ v) = v

-- all constraints are semimonoids
instance Semimonoidal (EnvC p) where
  ap2 (EnvC Dict p, EnvC Dict q) = EnvC Dict (p, q)

instance Monoid p => Monoidal (EnvC p) where
  ap0 = EnvC (Dict \\ (one :: () :- p))

instance Semimonad (EnvC p) where
  join (EnvC Dict p) = p

instance EnvC e -| (|=) e where
  adj = dimap (\eab a -> Constrained $ eab (EnvC Dict a))
              (\aeb (EnvC Dict a) -> runConstrained (aeb a))