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

[John Creighton]

On May 4, 9:46 am, Bartek Ćwikłowski <paczesi... at gmail.com> wrote:
> hello,
>
> 2010/5/4 John Creighton <johns2... at gmail.com>:
>
> > 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).
>
> Since Subset is the opposite of Superset, you can search in the
> "easier" (up) direction, so it really is as easy as reversing the
> order of arguments.
>
> It's not possible to write class/type-level function Child a b | a ->
> b, because functions (classes with fun-deps) must be deterministic. If
> you want to enumerate all children (based on Parent class instances),
> it's also impossible in this setup,

That's the approach I finally ended up taking. It seems to work so far
but I haven't tried using my child
function to build a subset or an isa function. My code is rather ugly
but it's the best I came up with. The
following are examples of the enumerations:


instance Parrent' () d Z Cat Feline --
instance Parrent' () d Z Feline Animal --

Z: means the first child
S Z: would be the second child instance
d is a type variable letting the relationship be bidirectional:
() is a dumby argument which is used in the case where their is no
instance.

It is used as follows:

instance (Parrent'' q d z anyChild anyParrent)=>Parrent' q d z
anyChild anyParrent

instance (ItsAnOrphan ~ anyParrent)=>Parrent'' q P1 n anyChild
anyParrent
instance (HasNoChildern ~ anyChild)=>Parrent'' q N1 Z anyChild
anyParrent
instance (HasNoMoreChildern ~ anyChild)=>Parrent'' q N1 (S n) anyChild
anyParrent

N1 is short for S Z
P1 is short for P Z (Negative numbers, P stands for previous)

> it's probably possible with Oleg's
> second-order typeclass programming[1].
>
> [1]http://okmij.org/ftp/Haskell/types.html#poly2


> But what are you actually trying to achieve? I can't thing of anything
> useful that would require walking down the hierarchy tree (and
> backtracking) and it has to be done at the type level.


Well, I need it for my Isa relationship defined so that

"a" isa "d" if their exists a "b" and "c" such that the following
conditions hold:

"a" isa subset of "b",
"b" isa "c"
"c" is a subset of "d"

Thus we know d, but we need to search backwards to find c.

Anyway, I don't have the code for isa or subset yet but here is my
code for child (some more testing warranted):
Any hints on making it cleaner or more readable would be appreciated.

-------------------------------------------------------------------------------------

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

{-# LANGUAGE TypeOperators #-} --10
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeSynonymInstances #-}
u=undefined
bla = child Z Animal
bla2 = child (u::P1) Animal
bla3 = child (u::Z) Cat
bla4 = child (u::P1) Cat
bla5 = parrent Cat
bla6 = parrent Feline
bla7 = parrent Animal
--20
-----------------------Instance SubType Relations
--------------------------------
data ItsAnOrphan = ItsAnOrphan
instance (Show ItsAnOrphan) where show _ = "ItsAnOrphan"

data HasNoMoreChildern = HasNoMoreChildern
instance (Show HasNoMoreChildern) where show _ = "HasNoMoreChildern"

data HasNoChildern = HasNoChildern
instance (Show HasNoChildern) where show _ = "HasNoChildern"


--30
class Parrent' () P1 Z a b =>Parrent a b| a->b where -- Specific Cases
    parrent :: a->b --
instance Parrent' () P1 Z a b => Parrent a b where
    parrent _ = undefined::b
class Parrent' q d n a b | q d n a-> b, q d n b ->a
class Parrent'' q d n a b | q d n a -> b,q d n b -> a
--class Parrent''' q n a b | q n b -> a

instance Parrent' () d Z Cat Feline --
instance Parrent' () d Z Feline Animal --
instance (Parrent'' q d z anyChild anyParrent)=>Parrent' q d z
anyChild anyParrent

instance (ItsAnOrphan ~ anyParrent)=>Parrent'' q P1 n anyChild
anyParrent
instance (HasNoChildern ~ anyChild)=>Parrent'' q N1 Z anyChild
anyParrent
instance (HasNoMoreChildern ~ anyChild)=>Parrent'' q N1 (S n) anyChild
anyParrent




class Child n a b|n a->b  where  -- a2 is the parrent of b
   child :: n->a->b
   child _ _ = undefined::b
instance (
         Parrent' () N1 n b2 a,
         Child' b2 n a b --b2==b or b2=HasNoChildern or
b2==HasNoMoreChildern
         )=>
         Child n a b
class Child' b2 n a b | b2 n a -> b --a2==a or a2=HasNoChildern or
a2==HasNoMoreChildern
class Child'' q b2 n a b|q b2 n a b ->b
class Child''' q b2 n a b|q b2 n a b ->b

instance Child' HasNoChildern Z a HasNoChildern
instance Child' HasNoMoreChildern (S n) a HasNoMoreChildern
instance (b2~b) => Child' b2 n a b
--instance Child'' () b2 n a b => Child' b2 n a b

--instance (Child''' q b2 n a b)=>Child''' q b2 n a b


----------- 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
---------------------- Peno Numbers -------------------------

data Z=Z
type family Simple a
type instance Simple (P (S n)) = n
type instance Simple (S (P n)) = n
type instance Simple Z = Z
data S n = S n
data P n = P n
type P1 = S Z
type P2 = S P1
type P3 = S P2
type P4 = S P3
type N1 = P Z
type N2 = P N1
type N3 = P N2
type N4 = P N3

-----------------------Basic Type Declarations
---------------------------50

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

data Animal=Animal -- deriving (Show)
instance Show Animal where show _ = "Animal"
data Feline=Feline -- deriving (Show) --50
instance Show Feline where show _ = "Feline"
data Cat = Cat -- deriving (Show)
instance Show Cat where show _ = "Cat"

data Taby_Cat=Taby_Cat deriving (Show) --60

-----------------------  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