Liquid Haskell Relational Specification with inductive matrix data type and linear map semantics.

LiquidRel.hs

{-@ LIQUID "--no-totality" @-}
{-@ LIQUID "--no-termination" @-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE GADTs #-}

module LiquidRel where

import Data.Void
import Data.Kind
import GHC.TypeLits
import GHC.Generics
import Data.Type.Equality
import Data.List (transpose)
import Data.Functor.Contravariant

data Relation a b where
  Empty :: Relation Void Void
  One :: Bool -> Relation () ()
  Join :: Relation c b -> Relation d b -> Relation (Either c d) b
  Fork :: Relation a c -> Relation a d -> Relation a (Either c d)

deriving instance Show (Relation a b)

instance Eq (Relation a b) where
  Empty == Empty               = True
  (One a) == (One b)           = a == b
  (Join a b) == (Join c d)     = a == c && b == d
  (Fork a b) == (Fork c d)     = a == c && b == d
  x@(Fork _ _) == y@(Join _ _) = x == abideJF y
  x@(Join _ _) == y@(Fork _ _) = abideJF x == y

instance Num Bool where
  (+) = (||)
  (-) = subAux
    where
      subAux False True = False
      subAux True False = True
      subAux False False = False
      subAux True True = False
  (*) = (&&)
  negate = not

instance Num (Relation a b) where
  (+) = addR
  (-) = subR
  (*) = mulR
  negate = negateR

addR :: Relation a b -> Relation a b -> Relation a b
addR Empty Empty               = Empty
addR (One a) (One b)           = One (a || b)
addR (Join a b) (Join c d)     = Join (addR a c) (addR b d)
addR (Fork a b) (Fork c d)     = Fork (addR a c) (addR b d)
addR x@(Fork _ _) y@(Join _ _) = addR x (abideJF y)
addR x@(Join _ _) y@(Fork _ _) = addR (abideJF x) y

subR :: Relation a b -> Relation a b -> Relation a b
subR Empty Empty               = Empty
subR (One a) (One b)           = One (a `subAux` b)
  where
    subAux False True = False
    subAux True False = True
    subAux False False = False
    subAux True True = False
subR (Join a b) (Join c d)     = Join (subR a c) (subR b d)
subR (Fork a b) (Fork c d)     = Fork (subR a c) (subR b d)
subR x@(Fork _ _) y@(Join _ _) = subR x (abideJF y)
subR x@(Join _ _) y@(Fork _ _) = subR (abideJF x) y

mulR :: Relation a b -> Relation a b -> Relation a b
mulR Empty Empty               = Empty
mulR (One a) (One b)           = One (a && b)
mulR (Join a b) (Join c d)     = Join (mulR a c) (mulR b d)
mulR (Fork a b) (Fork c d)     = Fork (mulR a c) (mulR b d)
mulR x@(Fork _ _) y@(Join _ _) = mulR x (abideJF y)
mulR x@(Join _ _) y@(Fork _ _) = mulR (abideJF x) y

negateR :: Relation a b -> Relation a b
negateR Empty      = Empty
negateR (One a)    = One (not a)
negateR (Join a b) = Join (negateR a) (negateR b)
negateR (Fork a b) = Fork (negateR a) (negateR b)

instance Ord (Relation a b) where
    Empty <= Empty               = True
    (One a) <= (One b)           = a <= b
    (Join a b) <= (Join c d)     = (a <= c) && (b <= d)
    (Fork a b) <= (Fork c d)     = (a <= c) && (b <= d)
    x@(Fork _ _) <= y@(Join _ _) = x <= abideJF y
    x@(Join _ _) <= y@(Fork _ _) = abideJF x <= y

{-@ reflect abideJF @-}
abideJF :: Relation a b -> Relation a b
abideJF (Join (Fork a c) (Fork b d)) = Fork (Join (abideJF a) (abideJF b)) (Join (abideJF c) (abideJF d)) -- Join-Fork abide law
abideJF Empty                        = Empty
abideJF (One e)                      = One e
abideJF (Join a b)                   = Join (abideJF a) (abideJF b)
abideJF (Fork a b)                   = Fork (abideJF a) (abideJF b)

{-@ reflect comp @-}
comp :: Relation b c -> Relation a b -> Relation a c
comp Empty Empty           = Empty
comp (One a) (One b)       = One (a && b)
comp (Join a b) (Fork c d) = comp a c `addR` comp b d -- Divide-and-conquer law
comp (Fork a b) c          = Fork (comp a c) (comp b c) -- Fork fusion law
comp c (Join a b)          = Join (comp c a) (comp c b) -- Join fusion law

{-@ reflect tr @-}
tr :: Relation a b -> Relation b a
tr Empty      = Empty
tr (One e)    = One e
tr (Join a b) = Fork (tr a) (tr b)
tr (Fork a b) = Join (tr a) (tr b)

-- See https://github.com/bolt12/laop for more details



-- | Type family that computes the cardinality of a given type dimension.
--
--   It can also count the cardinality of custom types that implement the
-- 'Generic' instance.
type family Count (d :: Type) :: Nat where
  Count (Either a b)  = (+) (Count a) (Count b)
  Count (a, b)        = (*) (Count a) (Count b)
  Count (a -> b)      = (^) (Count b) (Count a)
  -- Generics
  Count (M1 _ _ f p)  = Count (f p)
  Count (K1 _ _ _)    = 1
  Count (V1 _)        = 0
  Count (U1 _)        = 1
  Count ((:*:) a b p) = Count (a p) * Count (b p)
  Count ((:+:) a b p) = Count (a p) + Count (b p)
  Count d             = Count (Rep d R)

-- | Type family that computes of a given type dimension from a given natural
--
--   Thanks to Li-Yao Xia this type family is super fast.
type family FromNat (n :: Nat) :: Type where
  FromNat 0 = Void
  FromNat 1 = ()
  FromNat n = FromNat' (Mod n 2 == 0) (FromNat (Div n 2))

type family FromNat' (b :: Bool) (m :: Type) :: Type where
  FromNat' 'True m  = Either m m
  FromNat' 'False m = Either () (Either m m)

-- | Type family that normalizes the representation of a given data
-- structure
type family Normalize (d :: Type) :: Type where
  Normalize (Either a b) = Either (Normalize a) (Normalize b)
  Normalize d            = FromNat (Count d)

-- | Constraint type synonyms to keep the type signatures less convoluted
type Countable a             = KnownNat (Count a)
type CountableDimensions a b = (Countable a, Countable b)
type Liftable a b            = (Eq b, Constructable a b, Enumerable a)
type Enumerable a            = (Enum a, Bounded a)
type ConstructNorm a         = (Enum a, Enum (Normalize a))
type ConstructableNorm a b   = (ConstructNorm a, ConstructNorm b)
type ConstructN a            = Construct (Normalize a)
type Constructable a b       = (Construct a, Construct b)
type ConstructableN a b      = (Construct (Normalize a), Construct (Normalize b))


----------------------------- Linear map semantics -----------------------------
newtype Vector e a = Vector { at :: a -> e }

instance Contravariant (Vector e) where
    contramap f (Vector g) = Vector (g . f)

instance Num e => Num (Vector e a) where
    fromInteger = Vector . const . fromInteger

    (+)    = liftV2 (+)
    (-)    = liftV2 (-)
    (*)    = liftV2 (*)
    abs    = liftV1 abs
    negate = liftV1 negate

liftV1 :: (e -> e) -> Vector e a -> Vector e a
liftV1 f x = Vector (f . at x)

liftV2 :: (e -> e -> e) -> Vector e a -> Vector e a -> Vector e a
liftV2 f x y = Vector (\a -> f (at x a) (at y a))

-- Semantics of Matrix e a b
type LinearMap a b = Vector Bool a -> Vector Bool b

semantics :: Relation a b -> LinearMap a b
semantics m = case m of
    Empty    -> id
    One e    -> const (Vector (const e))
    Join x y -> \v -> semantics x (Left >$< v) + semantics y (Right >$< v)
    Fork x y -> \v -> Vector $ either (at (semantics x v)) (at (semantics y v))

padLeft :: Num e => Vector e b -> Vector e (Either a b)
padLeft v = Vector $ \case Left _  -> 0
                           Right b -> at v b

padRight :: Num e => Vector e a -> Vector e (Either a b)
padRight v = Vector $ \case Left a  -> at v a
                            Right _ -> 0

dot :: (Num e, Enumerable a) => Vector e a -> Vector e a -> e
dot x y = sum [ at x a * at y a | a <- enumerate ]

--------------------------------- Construction ---------------------------------

class Construct a where
  row :: Vector Bool a -> Relation a ()

  linearMap :: Construct b => LinearMap a b -> Relation a b

instance Construct () where
  row v = One (at v ())

  linearMap m = col (m 1)

instance (Constructable a b) => Construct (Either a b) where
  row v = row (Left >$< v) `Join` row (Right >$< v)

  linearMap m = linearMap (m . padRight) `Join` linearMap (m . padLeft)

col :: (Construct a) => Vector Bool a -> Relation () a
col = tr . row

-- | Matrix builder function. Constructs a matrix provided with
-- a construction function that operates with canonical types.
matrixBuilder :: (Constructable a b, Enumerable a) => ((a, b) -> Bool) -> Relation a b
matrixBuilder f = linearMap $ \v -> Vector $ \b -> dot v $ Vector $ \a -> f (a, b)

-- | Lifts functions to matrices.
fromF :: Liftable a b => (a -> b) -> Relation a b
fromF f = matrixBuilder (\(a, b) -> if f a == b then 1 else 0)

-------------------------------- Deconstruction --------------------------------
enumerate :: Enumerable a => [a]
enumerate = [minBound .. maxBound]

basis :: (Enumerable a, Eq a) => [Vector Bool a]
basis = [ Vector (==a) | a <- enumerate ]

toLists' :: (Enumerable a, Enumerable b, Eq a) => Relation a b -> [[Bool]]
toLists' m = transpose
    [ [ at r i | i <- enumerate ] | c <- basis, let r = semantics m c ]

dump :: (Enumerable a, Enumerable b, Eq a) => Relation a b -> IO ()
dump = mapM_ print . toLists'

------------------------------- Normalised types -------------------------------
class Profunctor p where
    dimap :: (a -> b) -> (c -> d) -> p b c -> p a d

instance Profunctor (->) where
    dimap f g h = g . h . f

toNorm :: ConstructNorm a => a -> Normalize a
toNorm = toEnum . fromEnum

fromNorm :: ConstructNorm a => Normalize a -> a
fromNorm = toEnum . fromEnum

rowN :: (ConstructN a, ConstructNorm a) => Vector Bool a -> Relation (Normalize a) ()
rowN = row . contramap fromNorm

linearMapN :: (ConstructableN a b, ConstructableNorm a b)
           => LinearMap a b -> Relation (Normalize a) (Normalize b)
linearMapN = linearMap . dimap (contramap toNorm) (contramap fromNorm)

colN :: (ConstructN a, ConstructNorm a) => Vector Bool a -> Relation () (Normalize a)
colN = tr . rowN

-- | Matrix builder function. Constructs a matrix provided with
-- a construction function that operates with arbitrary types.
matrixBuilderN :: (ConstructableN a b, ConstructableNorm a b, Enumerable a)
               => ((a, b) -> Bool) -> Relation (Normalize a) (Normalize b)
matrixBuilderN f = linearMapN $ \v -> Vector $ \b -> dot v $ Vector $ \a -> f (a, b)

-- | Lifts functions to matrices with dimensions matching @a@ and @b@
-- cardinality's.

{-@ reflect fromFN @-}
fromFN :: (Eq b, ConstructableN a b, ConstructableNorm a b, Enumerable a)
       => (a -> b) -> Relation (Normalize a) (Normalize b)
fromFN f = matrixBuilderN (\(a, b) -> f a == b)


-- Relational combinators (Example)

-- | iden relation
{-@ reflect iden @-}
iden :: Liftable cols cols => Relation cols cols
iden = fromF id

-- | Relational inclusion (subset or equal)
{-@ reflect sse @-}
sse :: Relation a b -> Relation a b -> Bool
sse a b = a <= b

-- | Relational implication (the same as @'sse'@)
{-@ reflect implies @-}
implies :: Relation a b -> Relation a b -> Relation a b
implies r s = negate r `union` s

-- | Relational bi-implication
{-@ reflect iff @-}
iff :: Relation a b -> Relation a b -> Bool
iff r s = r == s

-- | Relational intersection
{-@ reflect intersection @-}
intersection :: Relation a b -> Relation a b -> Relation a b
intersection a b = a * b

-- | Relational union
{-@ reflect union @-}
union :: Relation a b -> Relation a b -> Relation a b
union a b = a + b

-- | Relation Kernel
{-@ reflect ker @-}
ker :: Relation a b -> Relation a a
ker r = tr r `comp` r

-- | Relation Image
{-@ reflect img @-}
img :: Relation a b -> Relation b b
img r = r `comp` tr r

-- Properties of relations

-- | A 'Relation' @r@ is 'reflexive' 'iff' @'id' ``sse`` r@
{-@ reflect reflexive @-}
reflexive :: Liftable a a => Relation a a -> Bool
reflexive r = iden <= r

-- | A 'Relation' @r@ is 'coreflexive' 'iff' @r ``sse`` 'id'@
{-@ reflect coreflexive @-}
coreflexive :: Liftable a a => Relation a a -> Bool
coreflexive r = r <= iden

-- | A 'Relation' @r@ is 'transitive' 'iff' @(r `.` r) ``sse`` r@
{-@ reflect transitive @-}
transitive :: Relation a a -> Bool
transitive r = (r `comp` r) `sse` r

-- | A 'Relation' @r@ is 'symmetric' 'iff' @r == 'tr' r@
{-@ reflect symmetric @-}
symmetric :: Relation a a -> Bool
symmetric r = r == tr r

-- Taxonomy of binary relations

-- | A 'Relation' @r@ is 'simple' 'iff' @'coreflexive' ('img' r)@
{-@ reflect simple @-}
simple :: Liftable b b => Relation a b -> Bool
simple = coreflexive . img

-- | A 'Relation' @r@ is 'injective' 'iff' @'coreflexive' ('ker' r)@
{-@ reflect injective @-}
injective :: Liftable a a => Relation a b -> Bool
injective = coreflexive . ker

-- | A 'Relation' @r@ is 'entire' 'iff' @'reflexive' ('ker' r)@
{-@ reflect entire @-}
entire :: Liftable a a => Relation a b -> Bool
entire = reflexive . ker

-- | A 'Relation' @r@ is 'surjective' 'iff' @'reflexive' ('img' r)@
{-@ reflect surjective @-}
surjective :: Liftable b b => Relation a b -> Bool
surjective = reflexive . img