ungadtagger-1.0.0: Abstract GADTs from typelevel tags

Safe HaskellSafe-Inferred

Data.GADT.Untagged

Synopsis

Documentation

data Untagged con Source

Existential type, representing GADT, abstracted from typelevel tag (first type parameter).

Constructors

forall a . Tagged (con a) 

untag :: con a -> Untagged conSource

Function to untag values.

 f :: [Term A] -> [Term B] -> [Untagged Term]
 f xs ys = map untag xs ++ map untag ys

match :: Untagged con -> (forall a. con a -> r) -> rSource

Processes untagged value by unpacking it from existential wrapper and feeding result to rank2-typed funarg.

  f :: Untagged Term -> Integer
  f term = match term $ \case
    Var ... -> ...
    Lam ... -> ...

data Untagged2 con Source

Existential type, representing GADT, abstracted from two typelevel tags (first two type parameters).

Constructors

forall a b . Tagged2 (con a b) 

untag2 :: con a b -> Untagged2 conSource

match2 :: Untagged2 con -> (forall a b. con a b -> r) -> rSource

data Untagged3 con Source

Existential type, representing GADT, abstracted from three typelevel tags (first three type parameters).

Constructors

forall a b c . Tagged3 (con a b c) 

untag3 :: con a b c -> Untagged3 conSource

match3 :: Untagged3 con -> (forall a b c. con a b c -> r) -> rSource