MatrixProd.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
import Data.Kind
import Data.Proxy
import Data.Singletons
import Data.Singletons.TypeLits
import Data.Type.Equality
import GHC.TypeLits

{-
data Matrix = Matrix { row :: Integer
                     , col :: Integer
                     }

prod :: Matrix -> Matrix -> Maybe Matrix
prod m1 m2
  | col m1 == row m2 = Just ...
  | otherwise        = Nothing
-}

-- 行列の形(行と列)を型レベルに持っておく．行列の中身は省略
data Matrix (row :: Nat) (col :: Nat) =
  Matrix
  { row :: Sing row
  , col :: Sing col
  }

instance Show (Matrix (row :: Nat) (col :: Nat)) where
  show m = show (fromSing $ row m) ++ " x " ++ show (fromSing $ col m)

-- 行列積(形が整合していることを型レベルで検査)
prod :: Matrix a b -> Matrix b c -> Matrix a c
prod m1 m2 = Matrix (row m1) (col m2)

{-
AgdaのΣ
record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁
-}
data Sigma a (b :: a -> Data.Kind.*) where
  Sigma :: SingKind a =>
           { proj1 :: Sing (x :: a)
           , proj2 :: b x
           } -> Sigma a b

withProj1 :: Sigma a b -> (DemoteRep a -> r) -> r
withProj1 (Sigma {proj1 = p}) f = f . fromSing $ p

withProj2 :: Sigma a b -> (forall x . b (x :: a) -> r) -> r
withProj2 (Sigma {proj2 = p}) f = f p

{-
∃ : ∀ {a b} {A : Set a} → (A → Set b) → Set (a ⊔ b)
∃ = Σ _
-}
type Exist t = Sigma k (t :: k -> Data.Kind.*)

-- (型レベル)0と等しい(型レベルの)値が，なにかしら存在するという命題
existsNatEqualsZero :: Exist ((:~:) 0)
-- existsNatEqualsZero :: Sigma Nat ((:~:) 0)
-- と，その証明
existsNatEqualsZero = Sigma SNat Refl
-- existsNatEqualsZero = Sigma (SNat :: Sing 0) (Refl :: 0 :~: 0)
-- existsNatEqualsZero = Sigma (SNat :: Sing 1) (Refl :: 0 :~: 1) -- error

-- 「(型レベル)0と等しい(型レベルの)値」を値レベルで取り出したもの
value :: Integer
value = withProj1 existsNatEqualsZero id

-- 「(型レベル)0と等しい(型レベルの)値」が0と等しい証明
proof :: 0 :~: 0
proof = withProj2 existsNatEqualsZero f where
  f :: 0 :~: x -> 0 :~: 0
  f Refl = Refl

-- 形を隠す
newtype SomeMatrix' row = SomeMatrix' (Exist (Matrix row))
newtype SomeMatrix = SomeMatrix (Exist SomeMatrix')

withSomeMatrix :: SomeMatrix -> (forall row col . Matrix row col -> r) -> r
withSomeMatrix (SomeMatrix m) f = withProj2 m $ \(SomeMatrix' m') -> withProj2 m' f

instance Show SomeMatrix where
  show sm = withSomeMatrix sm show

readMatrix :: IO SomeMatrix
readMatrix = do
  line <- getLine
  let [a, b] = map read (words line) :: [DemoteRep Nat]
  withSomeSing a $ \sa ->
    withSomeSing b $ \sb ->
      return $ SomeMatrix (Sigma sa (SomeMatrix' (Sigma sb (Matrix sa sb))))

toProxy :: Sing a -> Proxy a
toProxy _ = Proxy

maybeProd :: SomeMatrix -> SomeMatrix -> Maybe SomeMatrix
maybeProd sm1 sm2 =
  withSomeMatrix sm1 $ \m1 ->
  withSomeMatrix sm2 $ \m2 ->
  case (m1, m2) of
    (Matrix r1 c1, Matrix r2 c2) ->
      case withKnownNat c1 $ withKnownNat r2 $ sameNat (toProxy c1) (toProxy r2) of
        Nothing   -> Nothing
        Just Refl -> Just (SomeMatrix (Sigma r1 (SomeMatrix' (Sigma c2 (prod m1 m2)))))

main :: IO ()
main = do
  m1 <- readMatrix
  m2 <- readMatrix
  case maybeProd m1 m2 of
    Nothing -> error "Invalid"
    Just m3 -> print m3