Skip to content

Instantly share code, notes, and snippets.

@mbloms
Last active December 23, 2017 23:33
Show Gist options
  • Save mbloms/fddc012ba3ad0ea14db0eae49bd28bd2 to your computer and use it in GitHub Desktop.
Save mbloms/fddc012ba3ad0ea14db0eae49bd28bd2 to your computer and use it in GitHub Desktop.
Vectors and Matrices type parameterised over their length.
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
import Prelude hiding (tail, head)
import qualified Data.List as L
import Data.Coerce
import Control.Applicative hiding (empty)
import Control.Monad
import Control.Monad.Zip
class Peano t where
measure :: Integral a => t -> a
fromList :: [a] -> SafeList t a
data Zero
data Succ p
type P1 = Succ Zero
type P2 = Succ P1
type P3 = Succ P2
type P4 = Succ P3
type P5 = Succ P4
type P6 = Succ P5
type P7 = Succ P6
take1 :: [a] -> SafeList P1 a
take1 = fromList
take2 :: [a] -> SafeList P2 a
take2 = fromList
take3 :: [a] -> SafeList P3 a
take3 = fromList
take4 :: [a] -> SafeList P4 a
take4 = fromList
take5 :: [a] -> SafeList P5 a
take5 = fromList
take6 :: [a] -> SafeList P6 a
take6 = fromList
take7 :: [a] -> SafeList P7 a
take7 = fromList
peal :: Succ a -> a
peal = undefined
instance Peano Zero where
measure _ = 0
fromList _ = empty
instance Peano p => Peano (Succ p) where
measure x = 1 + (measure.peal) x
fromList (x:xs) = x `cons` fromList xs
pzero :: Zero
pzero = undefined
psucc :: Peano a => a -> Succ a
psucc = undefined
newtype SafeList p a = List [a]
deriving (Show, Read, Eq, Ord, Functor, Foldable)
empty :: SafeList Zero a
empty = List []
cons :: a -> SafeList p a -> SafeList (Succ p) a
cons x (List xs) = coerce (x:xs)
uncons :: SafeList (Succ p) a -> (a,SafeList p a)
uncons (toList -> (x:xs)) = coerce (x, xs)
head :: SafeList (Succ p) a -> a
head = fst.uncons
tail :: SafeList (Succ p) a -> SafeList p a
tail (List (_:xs)) = coerce xs
transpose :: Matr m n a -> Matr n m a
transpose = coerce.L.transpose. (coerce :: Matr m n a -> [[a]])
toList :: SafeList m a -> [a]
toList = coerce
toList2 :: Matr m n a -> [[a]]
toList2 = coerce
fromList2 :: (Peano n, Peano m) => [[a]] -> Matr m n a
fromList2 = fromList . map fromList
identity :: (Peano n, Num a) => Matr n n a
identity = fromList . map fromList $ iterate (0:) (1:repeat 0)
class Det t a where
det :: Num a => t -> a
instance {-# OVERLAPS #-} Det (SafeList P2 (SafeList P2 a)) a where
det (coerce -> [[a,b],[c,d]]) = a*d - b*c
instance Det (SafeList n (SafeList n a)) a => Det (SafeList (Succ n) (SafeList (Succ n) a)) a where
det lsts = sum $ do
(x,m) <- zip (zipWith (*) (cycle [1,-1]) (toList $ fmap head lsts)) (toList . reduceS . fmap tail $ lsts)
return (x * det m)
reduceS :: SafeList (Succ m) a -> SafeList (Succ m) (SafeList m a)
reduceS = coerce.reduce.toList
reduce :: [a] -> [[a]]
reduce [] = []
reduce (x:xs) = xs : do
lst <- reduce xs
return (x:lst)
bajs = bajs
instance {-# OVERLAPS #-} Applicative (SafeList P1) where
pure x = List [x]
liftA2 f (head -> a) (head -> b) = pure $ f a b
instance Applicative (SafeList n) => Applicative (SafeList (Succ n)) where
pure x = cons x $ pure x
liftA2 f (List as) (List bs) = List $ zipWith f as bs
instance {-# OVERLAPS #-} Monad (SafeList P1) where
(head -> x) >>= f = f x
instance Monad (SafeList n) => Monad (SafeList (Succ n)) where
(uncons -> (x,xs)) >>= f = head (f x) `cons` (xs >>= (tail . f))
instance Monad (SafeList n) => MonadZip (SafeList n) where
mzipWith = liftA2
type Matr m n a = SafeList m (SafeList n a)
mul :: (Num a, Monad (SafeList m), Monad (SafeList r), Monad (SafeList n))
=> Matr m r a -> Matr r n a -> Matr m n a
mul xs ys = do
x <- xs
return $ do
y <- transpose ys
return $ sum $ liftA2 (*) x y
jonas :: (Monad (SafeList a), Monad (SafeList b), Monad (SafeList c))
=> Matr b a Int -> Matr c b Int -> SafeList a (SafeList b (SafeList c Int))
jonas xs ys = do
x <- transpose xs
return $ do
y <- ys
let xx = _ $ pure1 x
let yy = _ $ pure1 y
return $ mul (xx :: Matr P3 P1) (yy :: Matr P1 P3)
--return $ (mul :: Matr P3 P1 Int -> Matr P1 P3 Int -> Matr P3 P3 Int) (fmap pure x) (pure y)
pure1 :: w -> SafeList P1 w
pure1 = pure
j :: Matr P3 P3 Int
j = List [List [1,1,1],List [2,2,2],List [3,3,3]]
j1 :: Matr P3 P3 Int
j1 = List [List [1,2,3],List [4,5,6],List [7,8,9]]
j2 :: Matr P3 P3 Int
j2 = List [List [3,1,3],List [4,1,3],List [5,1,9]]
a :: Matr P2 P3 Int
a = List . map List $ [1,2,4]:[2,6,0]:[]
b :: Matr P3 P4 Int
b = List . map List $ [4,1,4,3]:[0,-1,3,1]:[2,7,5,2]:[]
add :: (Num a, Monad (SafeList m), Monad (SafeList n))
=> Matr m n a -> Matr m n a -> Matr m n a
add xs ys = liftA2 (liftA2 (+)) xs ys
data Nat t where
Z :: Nat t
S :: Nat t -> Nat (Succ t)
instance Bounded (Nat Zero) where
minBound = Z
maxBound = Z
instance Bounded (Nat t) => Bounded (Nat (Succ t)) where
minBound = Z
maxBound = S minBound
instance Enum (Nat Zero) where
toEnum 0 = Z
fromEnum Z = 0
instance Enum (Nat t) => Enum (Nat (Succ t)) where
toEnum 0 = Z
toEnum n | n > 0 = S (toEnum (n-1))
fromEnum Z = 0
fromEnum (S p) = succ (fromEnum p)
succ Z = S Z
succ (S p) = S $ succ p
pred (S Z) = Z
pred (S p) = S $ pred p
--newtype Elementary n a = E (SafeList n (SafeList n a))
-- deriving (Show, Read, Eq)
--
--mulrow :: (Num a, Monad (SafeList n)) => Nat n -> a -> SafeList n (SafeList n a)
--mulrow (S p) x = (1 `cons` pure 0) `cons` mulrow p x
--
--deriving instance Show (Nat t)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment