Mon Jan 11 21:52:49 UTC 2021

```> 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)
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"
-------------- next part --------------
A non-text attachment was scrubbed...
Name: FiniteFunctions.hs