Skip to content

Instantly share code, notes, and snippets.

@Pzixel
Forked from krendelhoff/Main.hs
Created December 9, 2021 10:14
Show Gist options
  • Save Pzixel/298f66ac0c1e62b833e65a8dde7f58e4 to your computer and use it in GitHub Desktop.
Save Pzixel/298f66ac0c1e62b833e65a8dde7f58e4 to your computer and use it in GitHub Desktop.
хаскельные типострадания
{-# 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!"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment