[Haskell-cafe] closed world instances, closed type families

[oleg at okmij.org]

Henning Thielemann wrote:
> However the interesting part of a complete case analysis on type level
> peano numbers was only sketched in section "8.4 Closed type
> families". Thus I tried again and finally found a solution that works
> with existing GHC extensions:

You might like the following message posted in January 2005
        http://www.haskell.org/pipermail/haskell-cafe/2005-January/008239.html
(the whole discussion thread is relevant).

In particular, the following excerpt

-- data OpenExpression env r where
--   Lambda :: OpenExpression (a,env) r -> OpenExpression env (a -> r);
--   Symbol :: Sym env r -> OpenExpression env r;
--   Constant :: r -> OpenExpression env r;
--   Application :: OpenExpression env (a -> r) -> OpenExpression env a ->
--                  OpenExpression env r

-- Note that the types of the efold alternatives are essentially
-- the "inversion of arrows" in the GADT declaration above
class OpenExpression t env r | t env -> r where
    efold :: t -> env
             -> (forall r. r -> c r) -- Constant
             -> (forall r. r -> c r) -- Symbol
             -> (forall a r. (a -> c r) -> c (a->r))  -- Lambda
             -> (forall a r. c (a->r) -> c a -> c r) -- Application
             -> c r


shows the idea of the switch, but on more complex example (using
higher-order rather than first-order language). That message has
anticipated the tagless-final approach.