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

On May 4, 9:46 am, Bartek Ćwikłowski wrote:

hello,

2010/5/4 John Creighton :

...

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