[Haskell-cafe] Set Operations In Haskell's Type System

[John Creighton]

This is partly a continuation from:

http://groups.google.ca/group/haskell-cafe/browse_thread/thread/4ee2ca1f5eb88e7a?hl=en#
and
http://hpaste.org/fastcgi/hpaste.fcgi/view?id=25265

Also of relevance:
http://groups.google.ca/group/haskell-cafe/browse_thread/thread/9cc8858a2e51a995?hl=en#
http://www.haskell.org/haskellwiki/GHC/AdvancedOverlap
http://homepages.cwi.nl/~ralf/HList/paper.pdf
http://okmij.org/ftp/Haskell/typecast.html
http://www.haskell.org/haskellwiki/User:ConradParker/InstantInsanity
http://okmij.org/ftp/Haskell/types.html (haven't looked at this link
yet)

I will continue to try to solve the problem on my own but at the
moment I'm able to get IsSuperSet to work but not the classes Isa,
Child and IsSubSet to work. Unlike set theory IsSubSet is not the same
as switching the order arguments in IsSuperSet because the searching
is done in the opposite direction. In one case we are searching the
parents and each child only has one parent. In the other Case we are
searching the children and each parent could have multiple children).

Bellow is my current code:

{-# LANGUAGE EmptyDataDecls,
             MultiParamTypeClasses,
             ScopedTypeVariables,
             FunctionalDependencies,
             OverlappingInstances,
             FlexibleInstances,
             UndecidableInstances,
             TypeFamilies #-}

{-# LANGUAGE TypeOperators #-} --10
{-# LANGUAGE FlexibleContexts #-}
--{-# LANGUAGE IncoherentInstances #-}
----------------------IsSubSet -----------------------------------
data ItsNotAParrent
class IsSubSet a b c | a b -> c where -- General Definition
    isSubSet :: a->b->c
class Child a b|b->a where {}

instance (
          Parrent b a2,
          TypeEq a2 a itsAParrent, --
          Child' itsAParrent a b
          ) => Child a b
class Child' itsAParrent a b where {}
instance (TypeCast b ItsNotAParrent)=>Child' F a b --No Childern
instance (TypeCast b c, Parrent c b)=>Child' T a b
instance (TypeCast b M)=>Child' itsAParrent a b --- Fail Case


instance (
           TypeEq ItsNotAParrent a itsNotAParrent,
           TypeEq a b iseq,
           IsSubSet' itsNotAParrent iseq a b c3 --
         ) =>
         IsSubSet a b c3 where --
         isSubSet a b = undefined::c3


class IsSubSet' itsNotAParrent iseq a b c| itsNotAParrent iseq a b ->
c where {}

instance (TypeCast c T)=>IsSubSet' F T a b c where {}
instance (TypeCast c F)=>IsSubSet' T iseq a b c where {} --Not sure
which logic value is best for this case.
instance (TypeCast c M)=>IsSubSet' itsNotAParrent iseq a b c where {}
--Fail Case

instance (
          Child a d,
          IsSubSet d b c
         )=>
         IsSubSet' F F a b c where {}
--bla11=isSubSet Cat Animal

-----------------------Isa
---------------------------------------------
class Isa' a b c|a b->c where {} --Direct Relationship
class Isa a b c|a b->c where
   isa::a->b->c
instance (
          Isa' a1 b1 c1,      --Direct Relationship
          IsSuperSet a1 a c2, --Check --20
          IsSuperSet b b1 c3, --
          Isa'' c1 c2 c3 a1 b1 c4 -- Decesion function --
         )=>Isa a b c4 where
         isa a b = undefined::c4

class Isa'' c1 c2 c3 a b c4|c1 c2 c3 a b->c4 where {}
--   isa :: c1->c2->c3->a->b->c4

instance Isa'' T T T a1 b1 T where {}
--   isa'' c1 c2 c3 a b = T --30
instance Isa'' F c2 c3 a1 b1 F where {} --
--   isa'' c1 c2 c3 a b = F
instance Isa'' c1 F c3 a1 b1 F where {}
--   isa'' c1 c2 c3 a b = F
instance Isa'' c1 c2 F a1 b1 F where {}
--   isa'' c1 c2 c3 a b = F

---------------- Instance Isa Relations
----------------------------------
instance Isa' Animal Noun T
instance (TypeCast F result) => Isa' a b result
-----------------Test Relationships
----------------------------------40
--bla6 = isa Cat Noun --
--bla4 = isa Cat Verb
-----------------------Basic Type Declarations
---------------------------

data Noun = Noun deriving (Show) --15
data Verb = Verb deriving (Show) --
data Adjactive = Adjactive deriving (Show)

data Animal=Animal deriving (Show)
data Feline=Feline deriving (Show) --50
data Cat = Cat deriving (Show)

data Taby_Cat=Taby_Cat deriving (Show)

-----------------------Instance SubType Relations
--------------------------------
data ItsAnOrphan = ItsAnOrphan

instance Show ItsAnOrphan where
   show _ = "ItsAnOrphan" --60

class Parrent a b| a->b where -- Specific Cases
    parrent :: a->b --

instance Parrent Cat Feline where --
   parrent a = Feline --40
instance Parrent Feline Animal where --
   parrent a = Animal --
instance (TypeCast result ItsAnOrphan) => Parrent anyChild result
where
   parrent a = undefined::result


----------------------- Generic subType Relations
------------------------------

class IsSuperSet a b c | a b -> c where -- General Definition
    isSuperSet :: a->b->c

--instance (TypeEq b Animal T,TypeEq c F T)=>IsSuperSet a b c where
--85
--   isSuperSet a b = F --
u=undefined

instance (
           TypeEq ItsAnOrphan b isOrphan,
           TypeEq a b iseq,
           IsSuperSet' isOrphan iseq a b c3 --
         ) =>
         IsSuperSet a b c3 where --S
         isSuperSet a b = undefined::c3
--         isSuperSet a b=(isSuperSet' (u::isaninmal) (u::iseq) (a::a)
(b::b))::c3

class IsSuperSet' isOrphan iseq a b c| isOrphan iseq a b -> c where {}
--    isSuperSet' :: isOrphan->iseq->a->b->c

instance (TypeCast c T)=>IsSuperSet' F T a b c where {}
--   isSuperSet'  isOrphan iseq a b = T

instance (TypeCast c F)=>IsSuperSet' T T a b c where {} --Not sure
which logic value is best for this case.
instance (
          Parrent b d,
          IsSuperSet a d c
         )=>
         IsSuperSet' F F a b c where {}
--         isSuperSet' isOrphan iseq  a b = (isSuperSet a ((parrent
(b::b))::d))::c

instance (TypeCast c F)=>IsSuperSet' T F a b c where {}
--   isSuperSet'  isOrphan iseq a b = F

----------- Logical Types ------------------

data T=T -- deriving (Show)
data F=F -- deriving (Show) --25
data M=M -- Fail case
instance Show T where show _ = "T"
instance Show F where show _ = "F"
instance Show M where show _ = "M"

class ToBool a where
   toBool :: a->Bool

instance ToBool T where
   toBool a = True

instance ToBool F where
   toBool a = False

-----------------------Loical Type Relations
-----------------------------
class TypeOr a b c|a b->c where
   typeOr :: a->b->c
instance TypeOr T T T where
   typeOr a b = T --50
instance TypeOr T F T where
   typeOr a b = T
instance TypeOr F T T where
   typeOr a b = T
instance TypeOr F F T where
   typeOr a b = T

-----------------------  OKMIJ
------------------------------------------

class TypeEq' () x y b => TypeEq x y b | x y -> b
instance TypeEq' () x y b => TypeEq x y b
class TypeEq' q x y b | q x y -> b --60
class TypeEq'' q x y b | q x y -> b

instance TypeCast b T => TypeEq' () x x b
instance TypeEq'' q x y b => TypeEq' q x y b
instance TypeEq'' () x y F

-- see http://okmij.org/ftp/Haskell/typecast.html
class TypeCast   a b   | a -> b, b->a   where typeCast   :: a -> b
class TypeCast'  t a b | t a -> b, t b -> a where typeCast'  :: t->a-
>b
class TypeCast'' t a b | t a -> b, t b -> a where typeCast'' :: t->a-
>b --70

instance TypeCast'  () a b => TypeCast a b where typeCast x =
typeCast' () x
instance TypeCast'' t a b => TypeCast' t a b where typeCast' =
typeCast''
instance TypeCast'' () a a where typeCast'' _ x  = x

----------------------- Testing Code --------------------------------

myCat=Cat
bla=isSuperSet Animal Cat
bla2=isSuperSet Cat Animal
bla3=isSuperSet Animal Noun
bla4=isSuperSet Noun Animal
bla5=isSuperSet Noun Noun