T1633.hs

{-# LANGUAGE GADTs               #-}
{-# LANGUAGE DeriveAnyClass      #-}
{-@ LIQUID "--max-case-expand=0" @-}
{-@ LIQUID "--no-totality"       @-}

module T1633 where

import Data.Void

data Relation a b where
  Empty :: Relation Void Void
  One :: Int -> 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 (Num)
-- Here I use a type 'Natural 0 1' but I wanted to try and refine the GADT.
{-@
data Relation a b where
  Empty :: Relation Void Void
  One :: {v:Int | v = 0 || v = 1} -> 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)
@-}

-- (Eq, Num, Ord, etc.. instances ...)

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 + 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