Create a gist now

Instantly share code, notes, and snippets.

{-# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment