{-# LANGUAGE TypeOperators, TypeFamilies, FlexibleContexts, UndecidableInstances #-}
module Gq where
import Prelude hiding (pred)
import BooleanAlgebra

data P -- the type of predicates

data T -- the type of truth values

data (:->) a b -- a :-> b is the type of functions from a to b

class Pred exp where
  pred :: Int -> exp P

class Name exp where
  name :: Int -> exp (P :-> T)

class GQ exp where
  everyone :: exp (P :-> T)
  someone :: exp (P :-> T)
  noone :: exp (P :-> T)

class Apply exp where
  ($>) :: exp (a :-> b) -> exp a -> exp b
  (<$) :: exp a -> exp (a :-> b) -> exp b
  (<$) = flip ($>)

data Model e t = Model {individuals :: Int -> e, predicates :: Int -> e -> t}

type family TypeInterp (e :: *) (t :: *) (ty :: *) :: *
type instance TypeInterp e t T = t
type instance TypeInterp e t P = e -> t
type instance TypeInterp e t (a :-> b) = TypeInterp e t a -> TypeInterp e t b

newtype Interp e t ty = Interp {unInterp :: Model e t -> TypeInterp e t ty}

instance Pred (Interp e t) where
  pred i = Interp (\model -> predicates model i)

instance Name (Interp e t) where
  name i = Interp (\model p -> p (individuals model i))

instance Apply (Interp e t) where
  Interp f $> Interp x = Interp (\model -> f model (x model))

instance Lattice (TypeInterp e t a) => Lattice (Interp e t a) where
  Interp f `meet` Interp g = Interp (f `meet` g)
  Interp f `join` Interp g = Interp (f `join` g)

instance Boolean (TypeInterp e t a) => Boolean (Interp e t a) where
  top = Interp top
  bot = Interp bot
  cmp (Interp f) = Interp (cmp f)

instance (Bounded e,Enum e,b~Bool) => GQ (Interp e b) where
  everyone = Interp (\_ p -> all p [minBound..maxBound])
  someone = Interp (\_ p -> any p [minBound..maxBound])
  noone = Interp (\_ p -> all (not . p) [minBound..maxBound])