Existential (dis)closure as (un)curry isomorphism

DisClo.hs

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]

clo :: (E -> DS) -> DS
clo f = \g -> [x:xs | x <- dom, xs <- f x g]

-- (clo . dis) φ
-- (\f g -> [x:xs | x <- dom, xs <- f x g]) (dis φ)
-- \g -> [x:xs | x <- dom, xs <- dis φ x g]
-- \g -> [x:xs | x <- dom, xs <- [ys | x:ys <- φ g]]
-- \g -> [x:ys | x <- dom, x:ys <- φ g]
-- \g -> φ g                                            -- dom ~ E
-- φ

-- (dis . clo) f
-- (\φ x g -> [xs | x:xs <- φ g]) (clo f)
-- \x g -> [xs | x:xs <- clo f g]
-- \x g -> [xs | x:xs <- [y:ys | y <- dom, ys <- f y g]]
-- \x g -> [xs | x `elem` dom, xs <- f x g]             -- elem to avoid shadowing x
-- \x g -> f x g                                        -- dom ~ E
-- f

-- cf.
-- curry   :: ((a, b) -> c) -> a -> b -> c
-- uncurry :: (a -> b -> c) -> (a, b) -> c
-- lists are products of arbitrary lengths
-- dis is ~ currying   applied to output assignments
-- clo is ~ uncurrying applied to output assignments

data Var = X | Y | Z deriving (Eq, Show)
type G = Var -> E
type DG = G -> [G]

disV :: Var -> DG -> (E -> DG)
disV v φ = \x g -> [h | h <- φ g, h v == x]

cloV :: Var -> (E -> DG) -> DG
cloV v f = \g -> [modify h v x | x <- dom, h <- f x g]
  where modify h v x = \u -> if u == v then x else h u

-- (cloV v . disV v) φ
-- (\f g -> [modify h v x | x <- dom, h <- f x g]) (disV v φ)
-- \g -> [modify h v x | x <- dom, h <- disV v φ x g]
-- \g -> [modify h v x | x <- dom, h <- [h | h <- φ g, h v == x]]
-- \g -> [modify h v x | x <- dom, h <- φ g, h v == x]
-- \g -> [h | x <- dom, h <- φ g, h v == x]             -- h v already is x
-- \g -> [h | h <- φ g]                                 -- assuming total assignments
-- \g -> φ g
-- φ

-- (disV v . cloV v) f
-- (\φ x g -> [h | h <- φ g, h v == x]) (cloV v f)
-- \x g -> [h | h <- cloV v f g, h v == x]
-- \x g -> [h | h <- [modify h v x | x <- dom, h <- f x g], h v == x]
-- \x g -> [modify h v x | x `elem` dom, h <- f x g, h v == x]
-- \x g -> [h | x `elem` dom, h <- f x g, h v == x]     -- h v already is x
-- \x g -> [h | h <- f x g]                             -- assuming total assignments
-- \x g -> f x g
-- f

-- (dis . clo) f
-- (\φ x g -> [xs | x:xs <- φ g]) (clo f)
-- \x g -> [xs | x:xs <- clo f g]
-- \x g -> [xs | x:xs <- [y:ys | y <- dom, ys <- f y g]]
-- \x g -> [xs | x <- dom, xs <- f x g]
   -- there's some shadowing here that's confusing me
   -- don't you just want:
   -- \x g -> [xs | xs <- f x g]
   -- (the only y that would match the x:xs pattern is y = x)
-- \x g -> f x g                                        -- dom ~ E
                                                        -- do you need this? it's not just extensionality?
-- f