Re: [Haskell-cafe] A quick question about distribution of finite maps.
I find the idea that finite sets and functions may be represented in Haskell very attractive in general
Okay, so the Map was a red herring. It is only one possible implementation of the mathematical concept you are after. To be more clear, let's use Map with capital M whenever we mean the data structure and "map" or "function" whenever we mean the mathematical concept. What you really want is functions between finite sets. Maps do not, in general, represent functions in the Control.Category sense. That got me hooked onto the Kleisli thing. Classical case of nerd-sniping. But you want to deviate from Control.Category and that's perfectly fine because we know the math works.
This establishes a Cartesian closed category of somewhat idealized entities. Can the realization of this category in Haskell be perfected to exclude pathologies by construction?
I think you need dependent types, but let's try. import Data.Map (Map) import qualified Data.Map.Strict as Map import Data.Set (Set) import qualified Data.Set as Set -- Note: One could also define -- FiniteFunction a b = (Set a, a -> b) -- hence the Map in your OP was misleading. newtype FiniteFunction a b = FMap {asMap :: Map a b} domain :: FiniteFunction a b -> Set a domain = Map.keysSet . asMap codomain :: Ord b => FiniteFunction a b -> Set b codomain = Set.fromList . Map.elems . asMap unsafeRunFiniteFunction :: Ord a => FiniteFunction a b -> a -> b unsafeRunFiniteFunction = (assertDomain.) . flip Map.lookup . asMap where assertDomain (Just b) = b assertDomain Nothing = error "argument outside of domain" -- | @(unsafeRunFiniteFunction f) `restrictedTo` (domain f) = f@ restrictedTo :: (a -> b) -> Set a -> FiniteFunction a b f `restrictedTo` dom = FMap (Map.fromSet f dom) -- | (.) of the category. -- 'id' on dom is @id `restrictedTo` dom@ compose :: (Ord a, Ord b, Ord c) => FiniteFunction b c -> FiniteFunction a b -> FiniteFunction a c compose (FMap g) (FMap f) = FMap (fmap g' f) where g' b = case Map.lookup b g of Nothing -> error "type mismatch between domain and codomain" Just c -> c {-- Now to the CCC structure. At this point we run into a problem: Categorically, if f :: A -> (C^B) and we uncurry it, then the domain of (uncurry f) is a square, the cartesian product of A and B. Trying to curry a function whose domain is a proper subset of the cartesian product of A and B should be a type error in my opinion, but Haskell's type system can not express this. I imagine failure of this property may lead to unexpected results when used in conjunction with 'compose'. But maybe currying functions with non-square domain is a desirable feature. If so, remove assertUncurried below. --} -- | @'isSquare' setOfPairs = True@ iff @setOfPairs@ -- is of the form -- @Set.fromList [(a,b) | a <- setA, b <- setB]@. isSquare :: (Ord a, Ord b) => Set (a,b) -> Bool isSquare setOfPairs = let fstProj = Set.map fst setOfPairs sndProj = Set.map snd setOfPairs in all (\a -> all (\b -> (a,b) `Set.member` setOfPairs) sndProj) fstProj isUncurried :: (Ord a, Ord b) => FiniteFunction (a,b) c -> Bool isUncurried = isSquare . domain -- | Beware: we can not express in the type system that -- for all keys @a@ the 'domain' :: Set b of the value under @a@ -- is the same Set, which is a prerequisite for the CCC operation. -- Hence we can not guarantee that the resulting 'domain' 'isSquare'. uncurryFiniteFunction :: (Ord a, Ord b) => FiniteFunction a (FiniteFunction b c) -> FiniteFunction (a,b) c uncurryFiniteFunction = FMap . Map.foldMapWithKey unc . asMap where unc a (FMap bc) = Map.mapKeysMonotonic ((,) a) bc -- | likewise, if the 'domain' of the uncurried function -- fails 'isSquare' then the result is not a well-defined -- higher-order 'FiniteFunction'. curryFiniteFunction :: (Ord a, Ord b) => FiniteFunction (a,b) c -> FiniteFunction a (FiniteFunction b c) curryFiniteFunction f@(FMap ab_c) = assertUncurried (FMap a_bc) where filterFst a = Map.foldMapWithKey (\ab c -> if fst ab == a then Map.singleton (snd ab) c else Map.empty) ab_c as = Map.foldMapWithKey (\(a,_) _ -> Set.singleton a) ab_c a_bc = Map.fromSet (FMap . filterFst) as assertUncurried = if isUncurried f then id else error "not an uncurried function"
Hello Olaf and everyone. This is awesome code, much more crisp than what I have been drafting. It highlights that we need to roll out our own dynamic type system to track that the domains of finite maps match where they should. I find it amusing and useful that we can have _«ragged»_ binary maps and currying still works in the absence of empty maps. So there is some space for future work — for instance, maybe non-trivial equality may remove this flaw. Other than that, I think the question is clarified!
On Mon, 2021-01-25 at 18:36 +0500, Ignat Insarov wrote:
Hello Olaf and everyone.
This is awesome code, much more crisp than what I have been drafting. It highlights that we need to roll out our own dynamic type system to track that the domains of finite maps match where they should.
I find it amusing and useful that we can have _«ragged»_ binary maps and currying still works in the absence of empty maps. Why that? There is Data.Map.empty and it represents any f `restrictedTo` Set.empty
So there is some space for future work — for instance, maybe non-trivial equality may remove this flaw. Other than that, I think the question is clarified! You could explore the design space of subtypes a bit further and let us know how it goes. For example, is FiniteFunction a b = (Set a, a -> b) feasible? Would TypeLevelNats be useful? What about (Set a, a -> b) where Set is a functor of subsets, such as in the infinite-search [*] package? For the special case where type a is a record, there is the records-sop package which has a binary IsSubTypeOf type relation.
Olaf [*] For any Eq type, the subsets that admit infinite search are finite.
participants (2)
-
Ignat Insarov -
Olaf Klinke