Algebra.hs

{-# LANGUAGE DataKinds, TypeOperators, StandaloneDeriving, KindSignatures, FlexibleInstances, FlexibleContexts, GADTs, TypeFamilies, UndecidableInstances
  #-}
module Algebra where
  
  type family Delete a b where
    Delete a '[] = '[]
    Delete a (a ': t) = Delete a t
    Delete a (h ': t) = h ': Delete a t

  type family Union a b where
    Union '[]        bs       = bs
    Union  as       '[]       = as
    Union (a ': as) (a ': bs) = a      ': Union (Delete a as) (Delete a bs)
    Union (a ': as) (b ': bs) = a ': b ': Union (Delete b as) (Delete a bs)


  data IsT a
  data AndT a b

  data Term :: [*] -> * -> * where 
    Is  :: a -> Term '[a] (IsT a)
    (:&:) :: Term t a -> Term u b -> Term (Union t u) (AndT a b)
  infixr 7 :&:

  instance Show a => Show (Term '[a] (IsT a)) where
    show (Is a) = show a
  instance (Show (Term t a), Show (Term u b), v ~ (Union t u)) => Show (Term v (AndT a b)) where
    show (a :&: b) = show a ++ " :&: " ++ show b

  instance Eq a => Eq (Term '[a] (IsT a)) where
    (Is a) == (Is b) = a == b
  instance (Eq (Term t a), Eq (Term u b), v ~ (Union t u)) => Eq (Term v (AndT a b)) where
    (a :&: b) == (c :&: d) = (a == c) && (b == d)

  newtype X = X Int deriving (Eq,Show)
  newtype Y = Y Int deriving (Eq,Show)
  newtype Z = Z Int deriving (Eq,Show)

  example :: Term '[X, Y] (AndT (IsT X) (AndT (IsT Y) (IsT X)))
  example = Is (X 3) :&: Is (Y 5) :&: Is (X 7)

Fixed.hs

{-# LANGUAGE DataKinds, TypeOperators, FlexibleInstances, GADTs, TypeFamilies, UndecidableInstances
  #-}
module Fixed where
  
  type family Delete a b where
    Delete a '[] = '[]
    Delete a (a ': t) = Delete a t
    Delete a (h ': t) = h ': Delete a t

  type family Union a b where
    Union '[]        bs       = bs
    Union  as       '[]       = as
    Union (a ': as) (a ': bs) = a      ': Union (Delete a as) (Delete a bs)
    Union (a ': as) (b ': bs) = a ': b ': Union (Delete b as) (Delete a bs)


  newtype E (t :: [*]) a = E a

  instance Eq a => Eq (E t a) where
    (E a) == (E b) = a == b
  instance Show a => Show (E t a) where
    show (E a) = show a



  data IsT a
  data AndT a b

  data Term :: * -> * where 
    Is  :: a -> Term (IsT a)
    (:&:) :: Term a -> Term b -> Term (AndT a b)
  infixr 7 :&:

  instance Show a => Show (Term (IsT a)) where
    show (Is a) = show a
  instance (Show (Term a), Show (Term b)) => Show (Term (AndT a b)) where
    show (a :&: b) = show a ++ " :&: " ++ show b

  instance Eq a => Eq (Term (IsT a)) where
    (Is a) == (Is b) = a == b
  instance (Eq (Term a), Eq (Term b)) => Eq (Term (AndT a b)) where
    (a :&: b) == (c :&: d) = (a == c) && (b == d)

  is :: a -> E '[a] (Term (IsT a))
  is a = E (Is a)

  (.&.) :: E t (Term a) -> E u (Term b) -> E (Union t u) (Term (AndT a b))
  infixr 7 .&.
  (E a) .&. (E b) = E (a :&: b)

  newtype X = X Int deriving (Eq,Show)
  newtype Y = Y Int deriving (Eq,Show)
  newtype Z = Z Int deriving (Eq,Show)

  example :: E '[X, Y] (Term (AndT (IsT X) (AndT (IsT Y) (IsT X))))
  example = is (X 3) .&. is (Y 5) .&. is (X 7)

GHCI Error Log

Algebra.hs:27:12:
    Could not deduce (v ~ Union t0 u0)
    from the context (Show (Term t a), Show (Term u b), v ~ Union t u)
      bound by an instance declaration:
                 (Show (Term t a), Show (Term u b), v ~ Union t u) =>
                 Show (Term v (AndT a b))
      at Algebra.hs:27:12-90
      ‘v’ is a rigid type variable bound by
          an instance declaration:
            (Show (Term t a), Show (Term u b), v ~ Union t u) =>
            Show (Term v (AndT a b))
          at Algebra.hs:27:12
    In the ambiguity check for an instance declaration:
      forall (v :: [*]) a b (t :: [*]) (u :: [*]).
      (Show (Term t a), Show (Term u b), v ~ Union t u) =>
      Show (Term v (AndT a b))
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In the instance declaration for ‘Show (Term v (AndT a b))’

Algebra.hs:32:12:
    Could not deduce (v ~ Union t0 u0)
    from the context (Eq (Term t a), Eq (Term u b), v ~ Union t u)
      bound by an instance declaration:
                 (Eq (Term t a), Eq (Term u b), v ~ Union t u) =>
                 Eq (Term v (AndT a b))
      at Algebra.hs:32:12-84
      ‘v’ is a rigid type variable bound by
          an instance declaration:
            (Eq (Term t a), Eq (Term u b), v ~ Union t u) =>
            Eq (Term v (AndT a b))
          at Algebra.hs:32:12
    In the ambiguity check for an instance declaration:
      forall (v :: [*]) a b (t :: [*]) (u :: [*]).
      (Eq (Term t a), Eq (Term u b), v ~ Union t u) =>
      Eq (Term v (AndT a b))
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In the instance declaration for ‘Eq (Term v (AndT a b))’