Something went wrong. Try again.
dependent-types proof-assistant
Something went wrong. Try again.
3.6 kB · 107 lines
Haskell
at main
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108
module Core.Experiments.Discrimination where
{-
Experiments on discrimination trees (dtree)
We probably want them for level values, where a level is basically "Map (Maybe Val) Integer",representing N₀ ⊔ (t₁ + N₁) ⊔ (t₂ + N₂) ⊔ ... ⊔ (tₙ + Nₙ) where Nᵢ are naturals and tᵢ are values.
There are several approaches to representing discrimination trees.1 There's a classic FP flavor that uses nested types. It's fine for many purposes, but it has some performance disadvantage, because some operations need to either allocate closures on every nesting, or use consecutive lookup/insert instead of in-place update.2 There's a version where we represent Map nesting explicitly as Mapᴺ for a runtime N integer. This is part of a known reduction of nested ADT-s to inductive families: https://gallais.github.io/blog/non-regular-parameters.html In Haskell it can be approximated either with Any and unsafe coercions, or with a "weakly typed tagged" representation, where we don't have type nesting but allow a bunch of illegal trees to be representable. The version with unsafe coercions is the most efficient, because we learn possible constructors at runtime from a plain Int and don't need extra layers of Haskell constructors.-}import Prelude hiding (lookup)import Common hiding (empty)
---------------------------------------------------------------------------------- Version with nested types and closure-free insertion.-- I try to make the generic implementation apparent.
data Tree = Leaf | Node2 Tree Tree | Node3 Tree Tree Tree deriving Show
data Map v = Map { mapLeaf :: Maybe v , mapNode2 :: Maybe (Map (Map v)) , mapNode3 :: Maybe (Map (Map (Map v))) } deriving (Show,Foldable)
makeFields ''Map
empty = Map Nothing Nothing Nothing
singleLeaf v = Just vsingleNode2 a b v = Just $ single a $ single b vsingleNode3 a b c v = Just $ single a $ single b $ single c v
single :: forall v. Tree -> v -> Map vsingle Leaf v = empty & leaf .~ singleLeaf vsingle (Node2 a b) v = empty & node2 .~ singleNode2 a b vsingle (Node3 a b c) v = empty & node3 .~ singleNode3 a b c v
lookup :: Tree -> Map v -> Maybe vlookup Leaf map = map^.leaflookup (Node2 a b) map = map^.node2 >>= lookup a >>= lookup blookup (Node3 a b c) map = map^.node3 >>= lookup a >>= lookup b >>= lookup c
update :: Tree -> v -> (v -> v) -> Map v -> Map vupdate = \t v f m -> case lookup t m of Nothing -> insert t v m Just v -> insert t (f v) m
-- Maybe a can be viewed as a partial (Map () a)updateMaybe :: a -> (a -> a) -> Maybe a -> Maybe aupdateMaybe = \a f -> \case Nothing -> Just a Just a' -> Just $ f a'
insert :: Tree -> v -> Map v -> Map vinsert Leaf v map = map & leaf %~ ( updateMaybe v $ id )insert (Node2 a b) v map = map & node2 %~ ( updateMaybe (single a $ single b v) $ update a (single b v) $ id )insert (Node3 a b c) v map = map & node3 %~ ( updateMaybe (single a $ single b $ single c v) $ update a (single b $ single c v) $ update b (single c v) $ update c v $ id )
mapToList :: Map v -> [(Tree, v)]mapToList m = do {v <- toList (m^.leaf); pure (Leaf, v)} ++ do {m <- toList (m^.node2); (a, m) <- mapToList m; (b, v) <- mapToList m; pure (Node2 a b, v)} ++ do {m <- toList (m^.node3); (a, m) <- mapToList m; (b, m) <- mapToList m; (c, v) <- mapToList m; pure (Node3 a b c, v)}
--------------------------------------------------------------------------------