[Haskell-cafe] closed world instances, closed type families
oleg at okmij.org
oleg at okmij.org
Wed Apr 3 05:23:55 CEST 2013
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.
More information about the Haskell-Cafe
mailing list