Skip to content

Instantly share code, notes, and snippets.

@cartazio cartazio/HBound.hs
Created Jun 7, 2013

Embed
What would you like to do?
Higher order bound http://hpaste.org/73764 hpaste by kmett
{-# LANGUAGE GADTs, Rank2Types, KindSignatures, ScopedTypeVariables, TypeOperators, DataKinds, PolyKinds, MultiParamTypeClasses, FlexibleInstances, TypeFamilies, DoRec, ExtendedDefaultRules #-}
import Control.Applicative
import Control.Category
import Control.Comonad
import Control.Monad.Fix
import Control.Monad (ap)
import Data.Functor.Identity
import Data.Typeable
import Data.Monoid
import Data.Unique
import System.IO.Unsafe
import Unsafe.Coerce
import Prelude hiding ((.),id)
infixl 1 >>>-, >>-
type Nat f g = forall x. f x -> g x
class HFunctor t where
hmap :: Nat f g -> Nat (t f) (t g)
class HFunctor t => HTraversable t where
htraverse :: Applicative m => (forall x. f x -> m (g x)) -> t f a -> m (t g a)
class HFunctor t => HMonad t where
hreturn :: Nat f (t f)
(>>-) :: t f a -> Nat f (t g) -> t g a
infixr 1 -<<
(-<<) :: HMonad t => Nat f (t g) -> Nat (t f) (t g)
f -<< m = m >>- f
class HBound s where
(>>>-) :: HMonad t => s t f a -> Nat f (t g) -> s t g a
class HMonadTrans s where
hlift :: HMonad t => Nat (t f) (s t f)
data Var b f a where
B :: b a -> Var b f a
F :: f a -> Var b f a
instance HFunctor (Var b) where
hmap _ (B b) = B b
hmap f (F a) = F (f a)
instance HTraversable (Var b) where
htraverse _ (B b) = pure (B b)
htraverse f (F a) = F <$> f a
instance HMonad (Var b) where
hreturn = F
B b >>- _ = B b
F a >>- f = f a
newtype Scope b t f a = Scope { unscope :: t (Var b (t f)) a }
instance HFunctor t => HFunctor (Scope b t) where
hmap f (Scope b) = Scope (hmap (hmap (hmap f)) b)
instance HTraversable t => HTraversable (Scope b t) where
htraverse f (Scope b) = Scope <$> htraverse (htraverse (htraverse f)) b
instance HMonad t => HMonad (Scope b t) where
hreturn = Scope . hreturn . F . hreturn
Scope e >>- f = Scope $ e >>- \v -> case v of
B b -> hreturn (B b)
F ea -> ea >>- unscope . f
instance HMonadTrans (Scope b) where
hlift = Scope . hreturn . F
instance HBound (Scope b) where
Scope m >>>- f = Scope (hmap (hmap (>>- f)) m)
data Equal a b where
Refl :: Equal a a
instance Category Equal where
id = Refl
Refl . Refl = Refl
abstract :: HMonad t => (forall x. f x -> Maybe (b x)) -> Nat (t f) (Scope b t f)
abstract f = Scope . hmap (\y -> case f y of
Just b -> B b
Nothing -> F (hreturn y))
instantiate :: HMonad t => Nat b (t f) -> Nat (Scope b t f) (t f)
instantiate k (Scope e) = e >>- \v -> case v of
B b -> k b
F a -> a
data Ix :: [*] -> * -> * where
Z :: Ix (a ': as) a
S :: Ix as b -> Ix (a ': as) b
data Vec :: (* -> *) -> [*] -> * where
HNil :: Vec f '[]
(:::) :: f b -> Vec f bs -> Vec f (b ': bs)
infixr 5 :++, :::
type family (:++) (as :: [*]) (bs :: [*]) :: [*]
type instance '[] :++ bs = bs
type instance (a ': as) :++ bs = a ': (as :++ bs)
happend :: Vec f as -> Vec f bs -> Vec f (as :++ bs)
happend HNil bs = bs
happend (a ::: as) bs = a ::: happend as bs
hsingleton :: f a -> Vec f '[a]
hsingleton x = x ::: HNil
instance HFunctor Vec where
hmap _ HNil = HNil
hmap f (x ::: xs) = f x ::: hmap f xs
instance HTraversable Vec where
htraverse _ HNil = pure HNil
htraverse f (x ::: xs) = (:::) <$> f x <*> htraverse f xs
class EqF f where
(==?) :: f a -> f b -> Maybe (Equal a b)
data Lit t where
Integer :: Integer -> Lit Integer
Double :: Double -> Lit Double
String :: String -> Lit String
value :: Lit a -> a
value (Integer i) = i
value (Double d) = d
value (String s) = s
class Literal a where
literal :: a -> Lit a
instance Literal Integer where
literal = Integer
instance Literal String where
literal = String
data Remote :: (* -> *) -> * -> * where
Var :: f a -> Remote f a
Lit :: Lit a -> Remote f a
Lam :: Scope (Equal b) Remote f a -> Remote f (b -> a)
Let :: Vec (Scope (Ix bs) Remote f) bs -> Scope (Ix bs) Remote f a -> Remote f a
Ap :: Remote f (a -> b) -> Remote f a -> Remote f b
lam_ :: EqF f => f a -> Remote f b -> Remote f (a -> b)
lam_ v f = Lam (abstract (v ==?) f)
lit :: Literal a => a -> Remote f a
lit = Lit . literal
instance HFunctor Remote where
hmap f (Var a) = Var (f a)
hmap _ (Lit t) = Lit t
hmap f (Lam b) = Lam (hmap f b)
hmap f (Let bs b) = Let (hmap (hmap f) bs) (hmap f b)
hmap f (Ap x y) = Ap (hmap f x) (hmap f y)
instance HTraversable Remote where
htraverse f (Var a) = Var <$> f a
htraverse _ (Lit t) = pure $ Lit t
htraverse f (Lam b) = Lam <$> htraverse f b
htraverse f (Let bs b) = Let <$> htraverse (htraverse f) bs <*> htraverse f b
htraverse f (Ap x y) = Ap <$> htraverse f x <*> htraverse f y
instance HMonad Remote where
hreturn = Var
Var a >>- f = f a
Lit t >>- _ = Lit t
Lam b >>- f = Lam (b >>>- f)
Let bs b >>- f = Let (hmap (>>>- f) bs) (b >>>- f)
Ap x y >>- f = Ap (x >>- f) (y >>- f)
(!) :: Vec f v -> Ix v a -> f a
(b ::: _) ! Z = b
(_ ::: bs) ! S n = bs ! n
eval :: Remote Identity a -> a
eval (Var w) = extract w
eval (Lit i) = value i
eval (Lam b) = \a -> eval (instantiate (\Refl -> Var (Identity a)) b)
eval (Let bs b) = eval (instantiate (vs !) b) where vs = hmap (instantiate (vs !)) bs
eval (Ap x y) = eval x (eval y)
closed :: HTraversable t => t f a -> Maybe (t g a)
closed = htraverse (const Nothing)
newtype V (a :: *) = V Unique
instance EqF V where
V a ==? V b
| a == b = Just (unsafeCoerce Refl)
| otherwise = Nothing
lam :: (Remote V a -> Remote V b) -> Remote V (a -> b)
lam f = unsafePerformIO $ do
x <- fmap V newUnique
return $ Lam $ abstract (x ==?) $ f $ Var x
data Binding a = V a := Remote V a
rhs :: Binding a -> Remote V a
rhs (_ := a) = a
data Bindings = forall bs. Bindings (Vec Binding bs)
elemIndex :: Vec Binding bs -> V a -> Maybe (Ix bs a)
elemIndex HNil _ = Nothing
elemIndex ((x := r) ::: xs) y = case x ==? y of
Just Refl -> Just Z
Nothing -> S <$> elemIndex xs y
instance Monoid Bindings where
mempty = Bindings HNil
Bindings xs `mappend` Bindings ys = Bindings (happend xs ys)
-- Allow the use of DoRec to define let statements
newtype Def a = Def { runDef :: IO (a, Bindings) }
instance Functor Def where
fmap f (Def m) = Def $ do
(a,w) <- m
return (f a, w)
instance Applicative Def where
pure = return
(<*>) = ap
instance Monad Def where
return a = Def $ return (a, mempty)
Def m >>= f = Def $ do
(a, xs) <- m
(b, ys) <- runDef (f a)
return (b, xs <> ys)
instance MonadFix Def where
mfix m = Def $ mfix $ \ ~(a, _) -> runDef (m a)
def :: Remote V a -> Def (Remote V a)
def v@Var{} = Def $ return (v, mempty) -- this thing already has a name
def r = Def $ do
v <- fmap V newUnique
return (Var v, Bindings (hsingleton (v := r)))
let_ :: Def (Remote V a) -> Remote V a
let_ (Def m) = unsafePerformIO $ do
(r, Bindings bs) <- m
return $ Let (hmap (abstract (elemIndex bs) . rhs) bs)
(abstract (elemIndex bs) r)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.