gistfile1.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
import Prelude hiding (init)

import Control.Applicative
import Data.Functor.Compose
import Data.Type.Equality
import Data.Monoid (Monoid(..), (<>))
import GHC.Exts (Constraint)
import Unsafe.Coerce

--------------------------------------------------------------------------------
data KV k v = KV k v

data KeyList :: (KV * *) -> * where
  KeysNil :: KeyList ('KV k v)
  KeysCons :: k -> KeyList ('KV k v) -> KeyList ('KV k v)

instance Monoid (KeyList ('KV k v)) where
  mempty = KeysNil
  mappend KeysNil xs = xs
  mappend (KeysCons x xs) ys = KeysCons x (mappend xs ys)

unKeyList :: KeyList ('KV k v) -> [k]
unKeyList KeysNil = []
unKeyList (KeysCons k ks) = k : unKeyList ks


--------------------------------------------------------------------------------
data Querying :: (* -> *) -> [KV * *] -> * -> * where
  Querying ::
    Applicative (ResultF (Reverse kvs))
      => Env kvs KeyList -> Compose m (ResultF (Reverse kvs)) a -> Querying m kvs a

instance (Functor m, Functor (ResultF (Reverse kvs))) => Functor (Querying m kvs) where
  fmap f (Querying kvs x) = Querying kvs (fmap f x)

instance (Applicative m, Applicative (ResultF (Reverse kvs)), Monoid (Env kvs KeyList)) => Applicative (Querying m kvs) where
  pure a = Querying mempty (pure a)
  (Querying kvs f) <*> (Querying kvs' x) = Querying (kvs <> kvs') (f <*> x)


--------------------------------------------------------------------------------
data ResultF :: [KV * *] -> * -> * where
  ResultFId :: a -> ResultF '[] a
  ResultComp :: ([(k, v)] -> ResultF kvs a) -> ResultF ('KV k v ': kvs) a

instance Functor (ResultF kvs) where
  fmap f (ResultFId x) = ResultFId (f x)
  fmap f (ResultComp x) = ResultComp (\kv -> fmap f (x kv))

instance Applicative (ResultF '[]) where
  pure a = ResultFId a
  (ResultFId f) <*> (ResultFId x) = ResultFId (f x)

instance Applicative (ResultF kvs) => Applicative (ResultF ('KV k v ': kvs)) where
  pure a = ResultComp (const (pure a))
  (ResultComp f) <*> (ResultComp x) = ResultComp (\kv -> f kv <*> x kv)


--------------------------------------------------------------------------------
data Query :: [KV * *] -> (KV * *) -> * where
  Here :: Query ('KV k v ': '[]) ('KV k v)
  There :: Query kvs kv -> Query (('KV x y) ': kvs) kv

deriving instance Show (Query kvs k)

class QueryToLast (kvs :: [KV * *]) where
  queryToLast :: Query kvs (Last kvs)

instance QueryToLast '[('KV k v)] where
  queryToLast = Here

instance (Last (('KV k v) ': kvs) ~ Last kvs, QueryToLast kvs) => QueryToLast ('KV k v ': kvs) where
  queryToLast = There queryToLast

type family HaveMatchingPrefixes (a :: [k]) (b :: [k]) :: Constraint where
  HaveMatchingPrefixes (x ': xs) (y ': ys) = (x ~ y, HaveMatchingPrefixes xs ys)
  HaveMatchingPrefixes xs        ys        = ()

reshape :: HaveMatchingPrefixes ts ts' => Env ts f -> Env ts' f -> Env ts' f
reshape Nil       xs        = xs
reshape _         Nil       = Nil
reshape (x :> xs) (_ :> ys) = x :> reshape xs ys


--------------------------------------------------------------------------------
withQuery
  :: ( QueryToLast (Snoc ('KV k v) kvs)
     , ('KV k v) ~ Last (Snoc ('KV k v) kvs)
     , Init (Snoc ('KV k v) kvs) ~ kvs
     , Reverse (Snoc ('KV k v) kvs) ~ (('KV k v) ': Reverse kvs)
     , Functor m, Monad m, Applicative (ResultF (Reverse kvs))
     )
  => ([k] -> m [(k, v)])
  -> (Query (Snoc ('KV k v) kvs) ('KV k v) -> Querying m (Snoc ('KV k v) kvs) a)
  -> Querying m kvs a
withQuery q k =
  case (k queryToLast) of
    (Querying kvs (Compose fIo)) ->
      case breakInit kvs of
        (kvs', keys) ->
          Querying kvs' $ Compose $ do ResultComp f <- fIo
                                       results <- q (unKeyList keys)
                                       return (f results)


runQuery :: (Monad m) => Querying m '[] a -> m a
runQuery (Querying Nil (Compose m)) = m >>= \(ResultFId a) -> return a


--------------------------------------------------------------------------------
data Env :: [k] -> (k -> *) -> * where
  Nil :: Env '[] f
  (:>) :: f t -> Env ts f -> Env (t ': ts) f

infixr 5 :>

instance Monoid (Env '[] f) where
  mempty = Nil
  mappend _ _ = Nil

instance (Monoid (Env ts f), Monoid (f t)) => Monoid (Env (t ': ts) f) where
  mempty = mempty :> mempty
  mappend (l :> ls) (r :> rs) = (l <> r) :> (mappend ls rs)

type family Snoc (a :: k) (as :: [k]) :: [k] where
  Snoc a '[] = '[a]
  Snoc a (x ': xs) = x ': (Snoc a xs)

type family Init (a :: [k]) :: [k] where
  Init '[] = '[]
  Init '[x] = '[]
  Init (x ': xs) = x ': Init xs

breakInit :: Env ts f -> (Env (Init ts) f, f (Last ts))
breakInit (x :> Nil) = (Nil, x)
breakInit (x :> (y :> ys)) = let (xs', t) = breakInit (y :> ys)
                             in (x :> xs', t)


--------------------------------------------------------------------------------
type family Last (a :: [k]) :: k where
  Last '[x] = x
  Last (x ': xs) = Last xs

type family Reverse (xs::[a]) :: [a]
type instance Reverse '[] = '[]
type instance Reverse (x ': xs) = Reverse xs ++ '[x]

type family (xs :: [a]) ++ (ys :: [a]) :: [a] where
  '[] ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)


--------------------------------------------------------------------------------
ask
  :: ( HaveMatchingPrefixes kvs kvs'
     , Monoid (Env kvs' KeyList)
     , Applicative (ResultF (Reverse kvs'))
     , Monad f
     )
  => Query kvs ('KV k v)
  -> k
  -> ResultF (Reverse kvs') a
  -> Querying f kvs' a
ask query k = Querying (reshape (mkEnv query k) mempty) . Compose . return
  where
  mkEnv :: Query kvs ('KV k v) -> k -> Env kvs KeyList
  mkEnv Here      key = KeysCons key KeysNil :> Nil
  mkEnv (There p) key = KeysNil :> mkEnv p key

mkResultF :: Eq k => Query kvs ('KV k v) -> k -> ResultF (Reverse kvs) (Maybe v)
mkResultF Here key = ResultComp (pure . lookup key)
mkResultF q@(There p) key =
  case mkResultF p key of
    ResultFId a -> pure a
    ResultComp c ->
      ResultComp $ \foo ->
       case c foo of
         ResultFId a -> pure a
         ResultComp c ->
           ResultComp $ \foo ->
            case c foo of
              ResultFId a -> pure a


--------------------------------------------------------------------------------
example :: Querying IO '[] (Maybe String, Maybe Int)
example =
  withQuery getUserNameById $ \userNameById ->
  withQuery getUserAgeById $ \userAgeById ->
    (,) <$> ask userNameById 1 (ResultComp $ const (ResultComp (pure . lookup 1)))
        <*> ask userAgeById 1 (mkResultF userAgeById 1)


  where
  getUserNameById :: [Int] -> IO [(Int, String)]
  getUserNameById = const (return [(1, "Hello")])

  getUserAgeById :: [Int] -> IO [(Int, Int)]
  getUserAgeById = const (return [(1, 5)])


main :: IO ()
main = runQuery example >>= print