mixst

Main.purs

module Main where

import Type.Prelude
import Type.Row
import Type.Data.Boolean
import Type.Data.Symbol as Symbol
import Data.Newtype

data RProxy (r :: # Type) = RProxy
data RLProxy (rl :: RowList) = RLProxy

newtype Field (guaranteed :: Boolean) typ = Field typ
derive instance newtypeField :: Newtype (Field g t) _

class Join
  (left   :: RowList)
  (right  :: RowList)
  (result :: RowList)
  | left right -> result
-- Fields are guaranteed if they are guaranteed on both sides
instance joinConsTrue ::
  -- ensure no duplicated fields
  ( RowListLacks label left'
  -- check if guaranteed in the other side, removing if it exists
  , IsGuaranteedIn label typ right there right'
  -- guaranteed if guaranteed on both sides
  , And here there guaranteed
  -- recurse!
  , Join left' right' result'
  ) => Join
    -- match on left
    (Cons label (Field here typ) left')
    -- preserve the right
    right
    -- add back on to the result
    (Cons label (Field guaranteed typ) result')
-- Any fields remaining in right do not occur in left, thus are not guaranteed
instance joinNil ::
  NonGuaranteed right result => Join Nil right result

class RowListLacks (key :: Symbol) (row :: RowList)
instance rowListLacks :: (RowLacks key r, ListToRow row r) => RowListLacks key row

-- | Set `guaranteed` to false in each field, preserving labels and types
class NonGuaranteed
  (row    :: RowList)
  (result :: RowList)
  | row -> result
instance nonGuaranteedCons ::
  ( NonGuaranteed row result
  ) => NonGuaranteed
    (Cons label (Field g     typ) row)
    (Cons label (Field False typ) result)
instance nonGuaranteedNil ::
  NonGuaranteed Nil Nil

-- | Check whether a field is guaranteed in a rowlist, requiring it to have the same type
class IsGuaranteedIn
  (label     ::  Symbol)
  (typ       ::    Type)
  (row       :: RowList)
  (result    :: Boolean)
  (remaining :: RowList)
  | row -> label typ result remaining
instance isGuaranteedInCons ::
  -- determine if this is the same field
  ( Symbol.Equals label lbl matches
  -- use the helper class to check the status of a match or recurse back here
  ,    IsGuaranteedInIf     matches label typ       lbl ty row  result              remaining
  ) => IsGuaranteedIn               label typ (Cons lbl ty row) result (Cons lbl ty remaining)
instance isGuaranteedInNil ::
  IsGuaranteedIn label typ Nil False Nil

-- Mutually recursive with IsGuaranteed
class IsGuaranteedInIf
  (matches   :: Boolean)
  (label     ::  Symbol)
  (typ       ::    Type)
  (lbl       ::  Symbol)
  (ty        ::    Type)
  (row       :: RowList)
  (result    :: Boolean)
  (remaining :: RowList)
  | matches -> label typ lbl ty row result remaining
instance isGuaranteedInIfTrue ::
  -- ensure this is a unique entry for the label
  ( RowListLacks             label                      row
  -- that matches the type in the other record
  , TypeEquals                     typ              ty
  ) => IsGuaranteedInIf True label typ lbl (Field g ty) row g row
instance isGuaranteedInIfFalse ::
  -- ignore this field, recurse into IsGuaranteedIn
  ( IsGuaranteedIn            label typ {-  -} row result remaining
  ) => IsGuaranteedInIf False label typ lbl ty row result remaining

test :: RProxy _
test = joinRow
  (RProxy :: RProxy (b :: Field True Int))
  (RProxy :: RProxy (a :: Field True Int))

{-
error :: RProxy _
error = joinRow
  (RProxy :: RProxy (a :: Field True Number))
  (RProxy :: RProxy (a :: Field True Int))
-}

rowToList :: forall r rl. RowToList r rl => RProxy r -> RLProxy rl
rowToList _ = RLProxy

listToRow :: forall r rl. ListToRow rl r => RLProxy rl -> RProxy r
listToRow _ = RProxy

join :: forall a b c. Join a b c => RLProxy a -> RLProxy b -> RLProxy c
join _ _ = RLProxy

joinRow ::
  forall a b c x y z.
    RowToList a x =>
    RowToList b y =>
    Join x y z =>
    ListToRow z c =>
  RProxy a -> RProxy b -> RProxy c
joinRow a b = listToRow (join (rowToList a) (rowToList b))