join と meet

TAPL 16.3.2 結びと交わりを計算するアルゴリズム。だいたいこんな感じ。

module JoinMeet where

import Data.Function
import Data.Map (Map)
import qualified Data.Map as Map

type Label = String

data Ty
  = TyTop
  | TyBool
  | TyArr Ty Ty
  | TyRcd (Map Label Ty)
  deriving Show

join :: Ty -> Ty -> Ty
join TyBool TyBool = TyBool
join (TyArr s1 s2) (TyArr t1 t2) = TyArr m1 j2
  where
    m1 = meet s1 t1
    j2 = join s2 t2
join (TyRcd s) (TyRcd t) = TyRcd $ foldr go Map.empty js
  where
    js = Map.keys (s `Map.intersection` t)
    go lbl = Map.insert lbl $ (join `on` (Map.! lbl)) s t
join _ _ = TyTop

meet :: Ty -> Ty -> Ty
meet TyTop _ = TyTop
meet _ TyTop = TyTop
meet TyBool TyBool = TyBool
meet (TyArr s1 s2) (TyArr t1 t2) = TyArr j1 m2
  where
    j1 = join s1 t1
    m2 = meet s2 t2
meet (TyRcd s) (TyRcd t) = TyRcd $ foldr go Map.empty ms
  where
    ms = Map.keys (s `Map.union` t)
    go lbl = Map.insert lbl $ select lbl s t
meet _ _ = error "fail"

select :: Label -> Map Label Ty -> Map Label Ty -> Ty
select lbl s t
  | lbl `Map.member` s && lbl `Map.member` t = (meet `on` (Map.! lbl)) s t
  | lbl `Map.member` s = s Map.! lbl
  | lbl `Map.member` t = t Map.! lbl

-- { x:Bool }
exJoin :: Ty
exJoin = join ty1 ty2
  where
    ty1 = TyRcd $ Map.fromList [("x", TyBool), ("y", TyBool)]
    ty2 = TyRcd $ Map.fromList [("x", TyBool), ("z", TyBool)]

-- { x:Bool, y:Bool, z:Bool }
exMeet :: Ty
exMeet = meet ty1 ty2
  where
    ty1 = TyRcd $ Map.fromList [("x", TyBool), ("y", TyBool)]
    ty2 = TyRcd $ Map.fromList [("x", TyBool), ("z", TyBool)]