...

static-inv.hs

{-# LANGUAGE DataKinds, KindSignatures, TypeOperators, GADTs, TypeFamilies, UndecidableInstances #-}

{- about invariants -}
data NatPos = One | Succ NatPos

data SingleNatPos :: NatPos -> * where
    SingleOne  :: SingleNatPos One
    SingleSucc :: SingleNatPos natpos -> SingleNatPos (Succ natpos)

type family (m :: NatPos) |+| (n :: NatPos) :: NatPos where
    One      |+| y = Succ y
    (Succ x) |+| y = Succ (x |+| y)

type family (m :: NatPos) |<=| (n :: NatPos) :: Bool where
    One      |<=| One      = True
    One      |<=| (Succ y) = True
    (Succ x) |<=| One      = False
    (Succ x) |<=| (Succ y) = x |<=| y

type family (m :: NatPos) |/=| (n :: NatPos) :: Bool where
    One      |/=| One      = False
    One      |/=| (Succ y) = True
    (Succ x) |/=| One      = True
    (Succ x) |/=| (Succ y) = x |/=| y

type family (a :: Bool) |&&| (b :: Bool) :: Bool where
    True  |&&| True  = True
    True  |&&| False = False
    False |&&| True  = False
    False |&&| False = False

data Matrix :: * -> NatPos -> NatPos -> * where                    -- ~ Matrix<T, rows, columns>        --
    Last      :: SingleNatPos n -> a -> Matrix a One n             -- ~ Node<Leaf, x, Leaf>             --
    Above     :: Matrix a m n -> a -> Matrix a (Succ m) n          -- ~ Node<(Node ...), x, Leaf>       --
    Before    :: Matrix a m n -> Matrix a o p -> a -> Matrix a m p -- ~ Node<(Node ...), x, (Node ...)> --
    Join      :: Matrix a m n -> Matrix a m o -> Matrix a m (n |+| o)
    Transpose :: Matrix a m n -> Matrix a n m
    Times     :: Matrix a m n -> Matrix a n o -> Matrix a m o
    Plus      :: Matrix a m n -> Matrix a m n -> Matrix a m n
    Negative  :: Matrix a m n -> Matrix a m n
    SwapLines :: ((i |<=| m) |&&| (j |<=| m) |&&| (i |/=| j)) ~ True => Matrix a m n -> SingleNatPos i -> SingleNatPos j -> Matrix a m n
    Identity  :: SingleNatPos n -> Matrix a n n
    -- etc... --

type Square a n = Matrix a n n

square :: Square a n -> ( )
square _ = ( )

{-

  *Main> square $ Before (Above (Last SingleOne 8) 12) (Last (SingleSucc SingleOne) 14) 22
  ()
  it :: ()
  (0.01 secs, 0 bytes)

-}

{-

  *Main> square $ Above (Last SingleOne 8) 12

  <interactive>:59:23:
    Couldn't match type ‘'One’ with ‘'Succ 'One’
    Expected type: SingleNatPos ('Succ 'One)
      Actual type: SingleNatPos 'One
    In the first argument of ‘Last’, namely ‘SingleOne’
    In the first argument of ‘Above’, namely ‘(Last SingleOne 8)’
  (0.00 secs, 0 bytes)

-}

{- about proofs  -}
type family Not (a :: Bool) :: Bool where
    Not True  = False
    Not False = True

type family (m :: NatPos) |==| (n :: NatPos) :: Bool where
    x |==| y = Not (x |/=| y)

data What :: NatPos -> * where
    What :: What natpos

instance Show (What (natpos :: NatPos)) where
    show What = "?"

data Proof :: Bool -> * where
    Accept :: Proof True
    Reject :: Proof False

add :: ((m |+| n) |==| (n |+| m)) ~ True => SingleNatPos m -> SingleNatPos n -> What (n |+| m)
add _ _ = What

{-

  *Main> add (SingleSucc SingleOne) (SingleSucc $ SingleSucc SingleOne)
  ?
  it :: What ('Succ ('Succ ('Succ ('Succ 'One))))
  (0.01 secs, 0 bytes)

-}

add' :: SingleNatPos m -> SingleNatPos n -> Proof ((m |+| n) |==| (n |+| m)) -> What (n |+| m)
add' _ _ _ = What

{-

  *Main> add' (SingleSucc SingleOne) (SingleSucc $ SingleSucc SingleOne) Accept
  ?
  it :: What ('Succ ('Succ ('Succ ('Succ 'One))))
  (0.01 secs, 0 bytes)

-}

{-

  *Main> :t add' (SingleSucc SingleOne) (SingleSucc $ SingleSucc SingleOne)
  add' (SingleSucc SingleOne) (SingleSucc $ SingleSucc SingleOne)
  :: Proof (('Succ 'One |+| 'Succ ('Succ 'One)) |==| ('Succ ('Succ 'One) |+| 'Succ 'One))
  -> What ('Succ ('Succ 'One) |+| 'Succ 'One)

-}

{-

*Main> add' (SingleSucc SingleOne) (SingleSucc $ SingleSucc SingleOne) Reject

<interactive>:21:65:
    Couldn't match type ‘'True’ with ‘'False’
    Expected type: Proof (('Succ 'One |+| 'Succ ('Succ 'One)) |==| ('Succ ('Succ 'One) |+| 'Succ 'One))
      Actual type: Proof 'False
    In the third argument of ‘add'’, namely ‘Reject’
    In the expression:
      add' (SingleSucc SingleOne) (SingleSucc $ SingleSucc SingleOne) Reject
(0.01 secs, 0 bytes)

-}

loweq :: SingleNatPos n -> SingleNatPos m -> Proof (n |<=| m) -> ( )
loweq _ _ _ = ( )

{-

*Main> :t loweq (SingleSucc $ SingleSucc SingleOne) (SingleOne)
loweq (SingleSucc $ SingleSucc SingleOne) (SingleOne)
  :: Proof ('Succ ('Succ 'One) |<=| 'One) -> ( )

-}

{-

*Main> :t loweq (SingleSucc $ SingleSucc SingleOne) (SingleOne) Accept

<interactive>:1:55:
    Couldn't match type ‘'False’ with ‘'True’
    Expected type: Proof ('Succ ('Succ 'One) |<=| 'One)
      Actual type: Proof 'True
    In the third argument of ‘loweq’, namely ‘Accept’
    In the expression:
      loweq (SingleSucc $ SingleSucc SingleOne) (SingleOne) Accept

-}

{-

*Main> :t loweq (SingleSucc $ SingleSucc SingleOne) (SingleOne) Reject
loweq (SingleSucc $ SingleSucc SingleOne) (SingleOne) Reject :: ( )

-}