[ADP-3153] Add Embedding of Typ

lib/fine-types/fine-types.cabal

@@ -66,6 +66,7 @@ library
     , yaml
   exposed-modules:
     Language.FineTypes
+    Language.FineTypes.Embedding
     Language.FineTypes.Export.OpenAPI.Typ
     Language.FineTypes.Export.OpenAPI.Value
     Language.FineTypes.Module
@@ -76,6 +77,8 @@ library
     Language.FineTypes.Typ.Gen
     Language.FineTypes.Value
     Language.FineTypes.Value.Gen
+  other-modules:
+    Language.FineTypes.Elaborate
 
 test-suite unit
   import:      language, opts-exe
@@ -96,6 +99,7 @@ test-suite unit
   main-is:
     Spec.hs
   other-modules:
+    Language.FineTypes.EmbeddingSpec
     Language.FineTypes.Export.OpenAPI.TypSpec
     Language.FineTypes.ParserSpec
     Language.FineTypes.ValueSpec

lib/fine-types/src/Language/FineTypes/Elaborate.hs

@@ -0,0 +1,69 @@
+module Language.FineTypes.Elaborate
+    ( elaborates
+    ) where
+
+import Prelude
+
+import Language.FineTypes.Typ
+    ( Typ (..), OpTwo (..) )
+
+{-----------------------------------------------------------------------------
+    Elaboration
+------------------------------------------------------------------------------}
+-- | Type A elaborates type B if it adds more specific information,
+-- such as field or constructor names, while representing the same structure.
+--
+-- Specifically,
+--
+-- * Every type elaborates 'Abstract'.
+-- * A record type with field names elaborates a product.
+-- * A sum type with constructor names elaborates a disjoint sum.
+elaborates :: Typ -> Typ -> Bool
+elaborates _ Abstract = True
+elaborates (Var name1) (Var name2) = name1 == name2
+elaborates (Zero c1) (Zero c2) = c1 == c2
+elaborates (One op1 a1) (One op2 a2)
+    = op1 == op2 && elaborates a1 a2
+elaborates (Two op1 a1 b1) (Two op2 a2 b2)
+    = op1 == op2 && elaborates a1 a2 && elaborates b1 b2
+elaborates (ProductN fields) a
+    | Just components <- matchProduct a =
+        elaboratesSeq (map snd fields) components
+    | otherwise = False
+elaborates (SumN fields) a
+    | Just summands <- matchSum a =
+        elaboratesSeq (map snd fields) summands
+    | otherwise = False
+elaborates _ _ = False
+
+-- | Check whether a sequence of types elaborates another sequence.
+elaboratesSeq:: [Typ] -> [Typ] -> Bool
+elaboratesSeq [] [] = True
+elaboratesSeq (x:xs) (y:ys) = elaborates x y && elaboratesSeq xs ys
+elaboratesSeq _ _ = False
+
+-- | Match a type @X@ against a product @A1 × A2 × … × An@
+-- with at least two components.
+--
+-- Association does not matter, i.e. @(A × B) × C = A × (B × C)@ have
+-- the same components.
+matchProduct :: Typ -> Maybe [Typ]
+matchProduct typ = case typ of
+    e@(Two Product2 _ _) -> Just $ match e
+    _ -> Nothing
+  where
+    match (Two Product2 a b) = match a <> match b
+    match e = [e]
+
+-- | Match a type @X@ against a sum @A1 ⊎ A2 ⊎ … ⊎ An@
+-- with at least two summands.
+--
+-- Association does not matter, i.e. @(A ⊎ B) ⊎ C = A ⊎ (B ⊎ C)@ have
+-- the same summands.
+matchSum :: Typ -> Maybe [Typ]
+matchSum typ = case typ of
+    e@(Two Sum2 _ _) -> Just $ match e
+    _ -> Nothing
+  where
+    match (Two Sum2 a b) = match a <> match b
+    match e = [e]

lib/fine-types/src/Language/FineTypes/Embedding.hs

@@ -0,0 +1,256 @@
+{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
+{-# HLINT ignore "Use lambda-case" #-}
+module Language.FineTypes.Embedding where
+
+import Prelude
+
+import Control.Monad
+    ((>=>))
+import Language.FineTypes.Typ
+    ( Typ )
+import Language.FineTypes.Value
+
+import qualified Data.Map as Map
+import qualified Data.Set as Set
+import qualified Language.FineTypes.Typ as Typ
+
+{-----------------------------------------------------------------------------
+    Embedding
+------------------------------------------------------------------------------}
+-- | An 'Embedding' from a type A into a type B
+-- is a many-to-one correspondence from the second type to the first.
+--
+-- > from . to = id
+--
+-- See Wadler's introduction to Agda
+--  https://plfa.github.io/20.07/Isomorphism/#embedding
+data Embedding a b = Embedding
+    { to :: a -> b
+    , from :: b -> a
+    }
+
+-- | An 'EmbeddingV' is a dynamically typed embedding of 'Value' into 'Value'.
+--
+-- Specifically, if @a `hasTyp` ta@ and @typecheck e ta == Just tb@,
+-- then @to e a == b@ and @b `hasTyp tab@.
+--
+-- The result of @to e a@ can be 'undefined' if the value @a@ does
+-- not have the expected 'Typ', that is @typecheck e ta == Nothing tb@.
+data EmbeddingTyp = EmbeddingTyp
+    { embed :: Embedding Value Value
+        -- ^ Embedding of 'Value's from one 'Typ' into the other.
+    , typecheck :: Typ -> Maybe Typ
+        -- ^ Check whether the 'Embedding' works on the given 'Typ'.
+    }
+
+-- Design Question: Return the embedding as part of the type check?
+
+{-----------------------------------------------------------------------------
+    Functorial operations
+------------------------------------------------------------------------------}
+-- | Composition of embeddings. Right-to-left.
+--
+-- > to (embed (ebc <> eab)) = to (embed ebc) . to (embed eab)
+instance Semigroup EmbeddingTyp where
+    ebc <> eab = EmbeddingTyp
+        { embed = Embedding
+            { to = to (embed ebc) . to (embed eab)
+            , from = from (embed eab) . from (embed ebc)
+            }
+        , typecheck = typecheck eab >=> typecheck ebc
+        }
+
+instance Monoid EmbeddingTyp where
+    mempty = EmbeddingTyp
+        { embed = Embedding { to = id, from = id }
+        , typecheck = Just
+        }
+
+-- | Operate on the argument of an unary operation.
+map1 :: EmbeddingTyp -> EmbeddingTyp
+map1 ee = EmbeddingTyp
+    { embed = Embedding
+        { to = \a -> case a of
+            One x -> One (fmap' (to e) x)
+            _ -> error "Typ(e) error in: map1, to"
+        , from = \b -> case b of
+            One x -> One (fmap' (from e) x)
+            _ -> error "Typ(e) error in: map1, from"
+        }
+    , typecheck = \t -> case t of
+        Typ.One op a -> Typ.One op <$> typecheck ee a
+        _ -> Nothing
+    }
+  where
+    e = embed ee
+
+    fmap' :: (Value -> Value) -> OneF Value -> OneF Value
+    fmap' f (Option a) = Option (f <$> a)
+    fmap' f (Sequence a) = Sequence (f <$> a)
+    fmap' f (PowerSet a) = PowerSet (Set.map f a)
+
+
+-- | Operate on the first argument of a 'Product' or 'Sum'.
+first' :: EmbeddingTyp -> EmbeddingTyp
+first' ee = EmbeddingTyp
+    { embed = Embedding
+        { to = \a -> case a of
+            Product [x,y] -> Product [to e x, y]
+            Sum 0 x -> Sum 0 $ to e x
+            Sum 1 _ -> a
+            _ -> error "Typ(e) error in: first', to"
+        , from = \b -> case b of
+            Product [x2,y2] -> Product [from e x2, y2]
+            Sum 0 x2 -> Sum 0 $ from e x2
+            Sum 1 _ -> b
+            _ -> error "Typ(e) error in: first', from"
+        }
+    , typecheck = \t -> case t of
+        Typ.Two fun a0 b
+            | fun == Typ.Sum2 || fun == Typ.Product2
+                -> (\a1 -> Typ.Two fun a1 b) <$> typecheck ee a0
+        _ -> Nothing
+    }
+  where
+    e = embed ee
+
+-- | Operate on the first argument of a 'Product' or 'Sum'.
+second' :: EmbeddingTyp -> EmbeddingTyp
+second' ee = EmbeddingTyp
+    { embed = Embedding
+        { to = \a -> case a of
+            Product [x,y] -> Product [x, to e y]
+            Sum 0 _ -> a
+            Sum 1 y -> Sum 1 $ to e y
+            _ -> error "Typ(e) error in: second', to"
+        , from = \b -> case b of
+            Product [x2, y2] -> Product [x2, from e y2]
+            Sum 0 _ -> b
+            Sum 1 y2 -> Sum 1 $ from e y2
+            _ -> error "Typ(e) error in: second', from"
+        }
+    , typecheck = \t -> case t of
+        Typ.Two fun a b0
+            | fun == Typ.Sum2 || fun == Typ.Product2
+                -> Typ.Two fun a <$> typecheck ee b0
+        _ -> Nothing
+    }
+  where
+    e = embed ee
+
+-- | Associative law for products.
+--
+-- > (A × B) × C  =>  A × (B × C)
+assocR :: EmbeddingTyp
+assocR = EmbeddingTyp
+    { embed = Embedding
+        { to = \t -> case t of
+            Product [Product [a,b],c] -> Product [a, Product [b,c]]
+            _ -> error "Typ(e) error in: assocR, to"
+        , from = \t -> case t of
+            Product [a, Product [b,c]] -> Product [Product [a,b],c]
+            _ -> error "Typ(e) error in: assocR, from"
+        }
+    , typecheck = \t -> case t of
+        Typ.Two Typ.Product2 (Typ.Two Typ.Product2 a b) c
+            -> Just $ Typ.Two Typ.Product2 a (Typ.Two Typ.Product2 b c)
+        _ -> Nothing
+    }
+
+{-----------------------------------------------------------------------------
+    Basic algebra
+------------------------------------------------------------------------------}
+-- | Unit law for a monoid.
+--
+-- > () ↦0 A  =>  A
+unit0 :: Value -> EmbeddingTyp
+unit0 zero = EmbeddingTyp
+    { embed = Embedding
+        { to = \a -> case a of
+            Two (FiniteMap m)
+                -> Map.findWithDefault zero (Zero Unit) m
+            _ -> error "Typ(e) error in: unit0, to"
+        , from =
+            Two . FiniteMap . Map.singleton (Zero Unit)
+        }
+    , typecheck = \t -> case t of
+        Typ.Two Typ.FiniteSupport (Typ.Zero Typ.Unit) s -> Just s
+        _ -> Nothing
+    }
+
+-- | Exponential law(s)
+-- 
+-- > (A ⊎ B) ↦0 C  =>  (A ↦0 C) × (B ↦0 C)
+-- > (A ⊎ B) ↦  C  =>  (A ↦ C)  × (B ↦ C)
+exponential :: EmbeddingTyp
+exponential = EmbeddingTyp
+    { embed = Embedding
+        { to = \a -> case a of
+            Two (FiniteMap m) ->
+                Product
+                    [ Two $ FiniteMap (left m)
+                    , Two $ FiniteMap (right m)
+                    ]
+            _ -> error "Typ(e) error in: exponential, to"
+        , from = \b -> case b of
+            Product
+                [ Two (FiniteMap ml)
+                , Two (FiniteMap mr)
+                ]
+                -> Two $ FiniteMap (plus ml mr)
+            _ -> error "Typ(e) error in: exponential, from"
+        }
+    , typecheck = \t -> case t of
+        Typ.Two fun (Typ.Two Typ.Sum2 a b) c
+            | fun == Typ.FiniteSupport || fun == Typ.PartialFunction
+            -> Just $ Typ.Two Typ.Product2 (Typ.Two fun a c) (Typ.Two fun b c)
+        _ -> Nothing
+    }
+  where
+    plus ml mr
+        = Map.mapKeys (Sum 0) ml <> Map.mapKeys (Sum 1) mr
+
+    left = withKeys matchLeft
+    right = withKeys matchRight
+
+    withKeys f
+        = Map.mapKeys fromSum
+        . Map.mapMaybeWithKey f
+
+    fromSum (Sum _ x) = x
+    fromSum _ = error "exponential: expected Sum"
+
+    matchLeft (Sum 0 _) v = Just v
+    matchLeft _ _ = Nothing
+
+    matchRight (Sum 1 _) v = Just v
+    matchRight _ _ = Nothing
+
+{-----------------------------------------------------------------------------
+    Conversions
+------------------------------------------------------------------------------}
+-- | Representation of finite maps as sequences of pairs.
+--
+-- > A ↦ B   =>  (A × B)*
+-- > A ↦0 B   =>  (A × B)*
+representMap :: EmbeddingTyp
+representMap = EmbeddingTyp
+    { embed = Embedding
+        { to = \a -> case a of
+            Two (FiniteMap m) -> valueFromList (Map.toList m)
+            _ -> error "Typ(e) error in: representMap, to"
+        , from = \b -> case b of
+            One (Sequence xs) ->
+                Two $ FiniteMap
+                    $ Map.fromList [ (x,y) | Product [x,y] <- xs ]
+            _ -> error "Typ(e) error in: representMap, from"
+        }
+    , typecheck = \t -> case t of
+        Typ.Two Typ.PartialFunction a b
+            -> Just $ Typ.One Typ.Sequence (Typ.Two Typ.Product2 a b)
+        Typ.Two Typ.FiniteSupport a b
+            -> Just $ Typ.One Typ.Sequence (Typ.Two Typ.Product2 a b)
+        _ -> Nothing
+    }
+  where
+    valueFromList = One . Sequence . map (\(a,b) -> Product [a,b])