Exploring De Bruijn Indices.

Indices.hs

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE UndecidableInstances #-}

module Indices where

import Control.Monad
import Control.Monad.Trans
import Data.Maybe
import Data.Void

-- https://www.schoolofhaskell.com/user/edwardk/bound

newtype Scope f a = Scope { runScope :: f (Maybe (f a)) }
    deriving Functor

instance Show (f (Maybe (f a))) => Show (Scope f a) where
    showsPrec n (Scope body) = showParen (n > 10) $ \s ->
        "Scope " ++ showsPrec 11 body s

-- I am not exactly the biggest fan of the Functor-Applicative-Monad
-- hierarchy.
instance Monad f => Applicative (Scope f) where
    pure = Scope . pure . Just . pure
    f <*> x = f >>= (\f -> x >>= (\x -> return (f x)))

instance Monad f => Monad (Scope f) where
    Scope body >>= f = Scope (body >>= g)
        where
        g (Just body) = body >>= runScope . f
        g Nothing     = return Nothing

instance MonadTrans Scope where
    lift = Scope . return . Just

abstract :: (Eq a, Monad f) => a -> f a -> Scope f a
abstract x y = Scope (liftM f y)
    where
    f z = return z <$ guard (x /= z)

instantiate :: Monad f => f a -> Scope f a -> f a
instantiate x (Scope body) = body >>= fromMaybe x

type Name = String

data ExprF a
    = Lam (Scope ExprF a)
    | App (ExprF a) (ExprF a)
    | Var a
    deriving (Functor, Show)

instance Applicative ExprF where
    pure x = Var x
    f <*> x = f >>= (\f -> x >>= (\x -> return (f x)))

instance Monad ExprF where
    Lam body    >>= f = Lam (body >>= lift . f)
    App fun arg >>= f = App (fun >>= f) (arg >>= f)
    Var var     >>= f = f var

-- Closed expressions.
type Expr = ExprF Void

s :: Expr
s = Lam (Scope (Lam (Scope (Lam (Scope (App (App (Var (Just (Var (Just (Var Nothing))))) (Var Nothing)) (App (Var (Just (Var Nothing))) (Var Nothing))))))))

k :: Expr
k = Lam (Scope (Lam (Scope (Var (Just (Var Nothing))))))

i :: Expr
i = Lam (Scope (Var Nothing))

-- Invalid expressions don't typecheck:
--
--  invalid :: Expr
--  invalid = Lam (Var (Just Nothing))