type-settheory-0.1: Control/SMonad.hs

--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
--Module       : Type.SMonad
--Author       : Daniel Schüssler
--License      : BSD3
--Copyright    : Daniel Schüssler
--
--Maintainer   : Daniel Schüssler
--Stability    : Experimental
--Portability  : Uses various GHC extensions
--
--------------------------------------------------------------------------------
--Description  : 
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------




{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}

-- | Example application of sets
--
-- This is quite similar to what the /rmonad/ package does, but we use preexisting sets rather than an associated datatype
--
-- * The apostrophed variants take proof objects as arguments
--
-- * The plain variants use 'auto'; that is, they assume that membership has been proved by an instance of 'Fact'
--
module Control.SMonad where
    
import Type.Set
import Type.Logic
import Data.Set as Set
    


class SFunctor dom f | f -> dom where
    sfmap' :: x :∈: dom ->
             y :∈: dom ->
                (x -> y) -> f x -> f y

class SFunctor dom f => SApplicative dom f | f -> dom where
    spure' :: x :∈: dom ->
            x -> f x

    sap' :: x :∈: dom ->
           y :∈: dom ->
           (x -> y) :∈: dom -> 
               
               f (x -> y) -> f x -> f y

class SApplicative dom m => SMonad dom m | m -> dom where
    sbind' :: x :∈: dom ->
             y :∈: dom ->
                 m x -> (x -> m y) -> m y
    
-- * Variants using auto for the domain-membership proofs

sfmap :: ( SFunctor dom f
        , Fact (x :∈: dom)
        , Fact (y :∈: dom) )
                     =>
                     (x -> y) -> f x -> f y
sfmap = sfmap' auto auto

spure :: ( SApplicative dom f
        , Fact (x :∈: dom) )
               
                     =>
                    x -> f x
spure = spure' auto

sap :: ( SApplicative dom f
        , Fact (x :∈: dom)
        , Fact (y :∈: dom)
        , Fact ((x -> y) :∈: dom) )
               
                     =>
                    f (x->y) -> f x -> f y
sap = sap' auto auto auto


sreturn' :: (SMonad dom f) => (x :∈: dom) -> x -> f x
sreturn' = spure'
           

sreturn :: (SMonad dom f, Fact (x :∈: dom)) => x -> f x
sreturn = spure

sbind
  :: (Fact (x :∈: dom), Fact (y :∈: dom), SMonad dom m) =>
     m x -> (x -> m y) -> m y
sbind = sbind' auto auto
        
-- * Derived combinators

sjoin'
  :: (SMonad dom m) => (m y :∈: dom) -> (y :∈: dom) -> m (m y) -> m y
sjoin' p1 p2 y = sbind' p1 p2 y id


sjoin
  :: (Fact (m y :∈: dom), Fact (y :∈: dom), SMonad dom m) =>
     m (m y) -> m y
sjoin y = sbind y id

-- | 'sfmap'' in terms of 'spure'' and 'sbind''
sfmap'Default
  :: (SMonad dom m) =>
     (x :∈: dom) -> (y :∈: dom) -> (x -> y) -> m x -> m y
sfmap'Default px py f x = sbind' px py x (\x0 -> sreturn' py (f x0))
                         
-- | 'sap'' in terms of 'spure'' and 'sbind''
sap'Default
  :: (SMonad dom m) =>
     (x :∈: dom)
     -> (y :∈: dom)
     -> ((x -> y) :∈: dom)
     -> m (x -> y)
     -> m x
     -> m y
sap'Default px py pxy f x = sbind' pxy py f
                             (\f0 -> sbind' px py x (\x0 -> sreturn' py (f0 x0)))




sliftA2'
  :: (SApplicative dom f) =>
       (x :∈: dom)
     -> (y :∈: dom)
     -> (z :∈: dom)
     -> ((y -> z) :∈: dom)
     -> (x -> y -> z)
     -> f x
     -> f y
     -> f z
sliftA2' px py pz pyz f x y = 

    sap' py pz pyz
    (sfmap' px pyz f x)
    y



sliftA2
  :: (Fact ((x1 -> y) :∈: dom),
      Fact (y :∈: dom),
      Fact (x1 :∈: dom),
      SApplicative dom f,
      Fact (x :∈: dom)) =>
     (x -> x1 -> y) -> f x -> f x1 -> f y
sliftA2 f x y = sfmap f x `sap` y


ssequence'
  :: (SApplicative dom f) =>
     (a :∈: dom)
     -> ([a] :∈: dom)
     -> (([a] -> [a]) :∈: dom)
       
     -> [f a]
     -> f [a]

ssequence' px pxs pxsxs = go
    where
      go [] = spure' pxs []
      go (x:xs) = sliftA2' px pxs pxs pxsxs (:) x (go xs)


ssequence
  :: (Fact (a :∈: dom),
      Fact ([a] :∈: dom),
      Fact (([a] -> [a]) :∈: dom),
      SApplicative dom f) =>
     [f a] -> f [a]
ssequence = ssequence' auto auto auto





instance SFunctor OrdType Set where
    sfmap' OrdType OrdType = Set.map

instance SApplicative OrdType Set where
    spure' OrdType = singleton
    sap' = sap'Default

instance SMonad OrdType Set where
    sbind' OrdType OrdType xs f = Set.fold (\x r -> Set.union (f x) r) Set.empty xs