📕

join と meet

2020/10/26に公開

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)]
``````