symantic/Language/Symantic/Interpreting/Dup.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE ConstraintKinds #-}
   3 -- | Interpreter to duplicate the representation of an expression
   4 -- in order to evaluate it with different interpreters.
   5 --
   6 -- NOTE: this is a more verbose, less clear,
   7 -- and maybe less efficient alternative
   8 -- to maintaining the universal polymorphism of @term@
   9 -- at parsing time as done with 'Term';
  10 -- it is mainly here for the sake of curiosity.
  11 module Language.Symantic.Interpreting.Dup where
  12
  13 -- | Interpreter's data.
  14 data Dup term1 term2 a
  15  =   Dup
  16  {   dup_1 :: term1 a
  17  ,   dup_2 :: term2 a
  18  }
  19
  20 dup0
  21  :: (cl r, cl s)
  22  => (forall term. cl term => term a)
  23  -> Dup r s a
  24 dup0 f = f `Dup` f
  25
  26 dup1
  27  :: (cl r, cl s)
  28  => (forall term. cl term => term a -> term b)
  29  -> Dup r s a
  30  -> Dup r s b
  31 dup1 f (a1 `Dup` a2) =
  32         f a1 `Dup` f a2
  33
  34 dup2
  35  :: (cl r, cl s)
  36  => (forall term. cl term => term a -> term b -> term c)
  37  -> Dup r s a
  38  -> Dup r s b
  39  -> Dup r s c
  40 dup2 f (a1 `Dup` a2) (b1 `Dup` b2) =
  41         f a1 b1 `Dup` f a2 b2
  42
  43 dup3
  44  :: (cl r, cl s)
  45  => (forall term. cl term => term a -> term b -> term c -> term d)
  46  -> Dup r s a
  47  -> Dup r s b
  48  -> Dup r s c
  49  -> Dup r s d
  50 dup3 f (a1 `Dup` a2) (b1 `Dup` b2) (c1 `Dup` c2) =
  51         f a1 b1 c1 `Dup` f a2 b2 c2