schar

import           Data.List
import           Prelude   hiding (max)

powerset :: [t] -> [[t]]
powerset []     = [[]]
powerset (x:xs) = powerset xs ++ map (x:) (powerset xs)

powersetPlus :: Eq t => [t] -> [[t]]
powersetPlus = filter (/= []) . powerset

schar

type E = Int
type T = Bool
type S = [E]
type R = [E] -> T
type Var = S -> E

data Form = Rel R [Var] | Ex | Not Form | And Form Form

eval :: Form -> S -> T
eval (Rel r ts) = \e -> r [t e | t <- ts]

schar

{-  That makes a lot of sense indeed. And the code becomes easier to
understand. Your original code is perhaps too advanced for this
task. I'm sending the simplified verison, requiring no extensions. It
is also easier to relate to the familiar De Bruijn indices, so it
should be easier to explain.  -}

module DBL1 where

import           Prelude hiding ((/))

schar

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE TupleSections #-}

module DBL where

import           Prelude hiding ((/))

-- indexed store coalgebra lenses

type Lens s t a b = s -> IStore a b t

schar

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE Rank2Types    #-}
{-# LANGUAGE TupleSections #-}

import           Control.Applicative
import           Control.Monad.Identity

{- Polymorphic van Laarhoven lenses -}

type LensFam a a' b b' = forall f. Functor f => (b -> f b') -> a -> f a'

schar

z   (x, _) = x
s n (_, h) = n h

-- NEW: indexed depositors
dz   x ((), r) = (x, r) -- novelty; () ~> _ = destructive updates
ds n x (y , r) = (y, n x r)

-- NEW: combinators for preallocating context
cinit = ()
cz    = cs cinit

schar

The de Bruijn index and level of a bound variable sum up to the number of
enclosing lambdas: i+l=n. Since the index can be recovered from the level by
subtraction, levels can be implemented as predecessor indices `p`:

> z :: (a, b) -> a
> z (x, _) = x

> s :: (a -> b) -> (c, a) -> b
> s v (_, h) = v h

schar

import Data.List

dom = [0..10]

type E = Int
type S = [Int]
type DS = S -> [S]

dis :: DS -> (E -> DS)
dis φ = \x g -> [xs | x:xs <- φ g]

schar

-- see https://stackoverflow.com/q/49322276/2684007

{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE MultiParamTypeClasses #-}

import           Control.Monad
import           Data.Functor
import           Data.Functor.Adjunction

newtype Three g f m a = Three { getThree :: g (m (f a)) }

schar

import           Control.Applicative
import           Control.Monad
import           Data.List

data Atom = P | Q | R | Top
  deriving (Show, Eq, Enum)

type W = [Atom]
type C = [W]
type Upd m = m C -> m C