хаскельные типострадания

Main.hs

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE KindSignatures      #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE TypeOperators       #-}
module Main where

import Data.Kind
import Prelude   (read)
import Universum hiding (Nat, Vector)

import qualified Data.Text as T

data Nat = Z | S Nat

data SNat (n :: Nat) where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)

toSNat :: Nat -> (forall n. SNat n -> r) -> r
toSNat Z f     = f SZ
toSNat (S n) f = toSNat n (f . SS)

toNat :: Int -> Nat
toNat n | n > 0 = S $ toNat $ n - 1
toNat _ = Z

data Vector (n :: Nat) (a :: Type) where
  VNil  :: Vector 'Z a
  VCons :: a -> Vector n a -> Vector ('S n) a

dotProduct :: Num a => Vector n a -> Vector n a -> a
dotProduct VNil VNil                 = 0
dotProduct (VCons x xs) (VCons y ys) = x * y + dotProduct xs ys

sumVecs :: Num a => Vector n a -> Vector n a -> Vector n a
sumVecs VNil VNil                 = VNil
sumVecs (VCons x xs) (VCons y ys) = VCons (x + y) $ sumVecs xs ys

printVec :: Show a => SNat n -> Vector n a -> IO ()
printVec SZ VNil = pass
printVec (SS n) (VCons x xs) = putStr @Text (show x) >> putStr @Text ","
                                                     >> printVec n xs

ones :: SNat n -> Vector n Int
ones SZ     = VNil
ones (SS n) = VCons 1 $ ones n

twos :: SNat n -> Vector n Int
twos SZ     = VNil
twos (SS n) = VCons 2 $ twos n

data (a :: k) :~: (b :: k) where
  Refl :: a :~: a

data a ?? b = Yes (a :~: b) | No

decEq :: SNat n -> SNat m -> n ?? m
decEq SZ SZ         = Yes Refl
decEq (SS n) SZ     = No
decEq SZ (SS n)     = No
decEq (SS n) (SS m) = case decEq n m of
                        (Yes Refl) -> Yes Refl
                        No         -> No

main :: IO ()
main = do
  n <- toNat . read . T.unpack <$> getLine
  m <- toNat . read . T.unpack <$> getLine
  toSNat n \lengthA ->
    toSNat m \lengthB -> case decEq lengthA lengthB of
                      Yes Refl -> do
                        putStr @Text "dot product:"
                        print $ dotProduct (ones lengthA) (twos lengthB)
                        printVec lengthA (sumVecs (ones lengthA) (twos lengthB))
                        putStrLn @Text ""
                      No -> putStrLn @Text "Cannot work on different lengths!"