{-# LANGUAGE ScopedTypeVariables, DeriveTraversable
, DeriveFunctor, DeriveFoldable, MonoLocalBinds #-}
{-# OPTIONS_GHC -Wall #-}
module Vec where
import Control.Exception.Base (assert)
import Data.Proxy
import Control.Applicative
import Data.Foldable
import Data.Traversable
-- Peano numbers
data N0
data Succ n
type N1 = Succ N0
type N2 = Succ N1
type N3 = Succ N2
type N4 = Succ N3
naturalPred :: Proxy (Succ n) -> Proxy n
naturalPred _ = Proxy
class Natural n where
fromNatural
:: Proxy n
-> Int
instance Natural N0 where
fromNatural _ = 0
instance Natural n => Natural (Succ n) where
fromNatural n = fromNatural (naturalPred n) + 1
-- fixed length lists
-- I'll only need lists of length up to 4
newtype V n a = V_ { get'V :: [a] }
deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
dim'V
:: forall n a
. Natural n
=> V n a
-> Int dim'V _ = fromNatural (Proxy :: Proxy n)
bad_fromList :: Natural n => [a] -> V n a
bad_fromList l = if length l == dim'V v
then v
else undefined -- this is line 11 where v = V_ l
bad
_f
:: Natural n
=> [a
] -> (V n a
, Int)bad_f xs = (v, dim'V v)
where v = V_ xs
good_f :: Natural n => a -> (V n a, Int)
good_f x = (v, dim'V v)
where v = V_ $ replicate (dim'V v) x
fromList'V :: forall n a. Natural n => [a] -> V n a
fromList'V l = assert (length l == dim'V v) v
where v = V_ l -- :: V n a -- why can't GHC infer this type?
instance Natural n => Applicative (V n) where
pure x = v
where v = V_ $ replicate (dim'V v) x -- GHC infers this type
(V_ fs) <*> (V_ xs) = V_ $ zipWithExact ($) fs xs
zipWithExact :: (a -> b -> c) -> [a] -> [b] -> [c]
zipWithExact _ [] [] = []
zipWithExact f (x:xs) (y:ys) = f x y : zipWithExact f xs ys
zipWithExact _ _ _ = error "zipWithExact: length mismatch"
ey0jIExBTkdVQUdFIFNjb3BlZFR5cGVWYXJpYWJsZXMsIERlcml2ZVRyYXZlcnNhYmxlCgksIERlcml2ZUZ1bmN0b3IsIERlcml2ZUZvbGRhYmxlLCBNb25vTG9jYWxCaW5kcyAjLX0KCnstIyBPUFRJT05TX0dIQyAtV2FsbCAjLX0KCm1vZHVsZSBWZWMgd2hlcmUgCgppbXBvcnQgQ29udHJvbC5FeGNlcHRpb24uQmFzZSAoYXNzZXJ0KQppbXBvcnQgRGF0YS5Qcm94eQppbXBvcnQgQ29udHJvbC5BcHBsaWNhdGl2ZSAKaW1wb3J0IERhdGEuRm9sZGFibGUKaW1wb3J0IERhdGEuVHJhdmVyc2FibGUKCi0tIFBlYW5vIG51bWJlcnMKZGF0YSBOMApkYXRhIFN1Y2MgbgoKdHlwZSBOMSA9IFN1Y2MgTjAKdHlwZSBOMiA9IFN1Y2MgTjEKdHlwZSBOMyA9IFN1Y2MgTjIKdHlwZSBONCA9IFN1Y2MgTjMKCm5hdHVyYWxQcmVkIDo6IFByb3h5IChTdWNjIG4pIC0+IFByb3h5IG4KbmF0dXJhbFByZWQgXyA9IFByb3h5CgpjbGFzcyBOYXR1cmFsIG4gd2hlcmUKICBmcm9tTmF0dXJhbCA6OiBQcm94eSBuIC0+IEludAoKaW5zdGFuY2UgTmF0dXJhbCBOMCB3aGVyZQogIGZyb21OYXR1cmFsIF8gPSAwCgppbnN0YW5jZSBOYXR1cmFsIG4gPT4gTmF0dXJhbCAoU3VjYyBuKSB3aGVyZQogIGZyb21OYXR1cmFsIG4gPSBmcm9tTmF0dXJhbCAobmF0dXJhbFByZWQgbikgKyAxCgotLSBmaXhlZCBsZW5ndGggbGlzdHMKLS0gSSdsbCBvbmx5IG5lZWQgbGlzdHMgb2YgbGVuZ3RoIHVwIHRvIDQKCm5ld3R5cGUgViBuIGEgPSBWXyB7IGdldCdWIDo6IFthXSB9CiAgZGVyaXZpbmcgKFNob3csIEVxLCBPcmQsIEZ1bmN0b3IsIEZvbGRhYmxlLCBUcmF2ZXJzYWJsZSkKCmRpbSdWIDo6IGZvcmFsbCBuIGEuIE5hdHVyYWwgbiA9PiBWIG4gYSAtPiBJbnQKZGltJ1YgXyA9IGZyb21OYXR1cmFsIChQcm94eSA6OiBQcm94eSBuKQoKCmJhZF9mcm9tTGlzdCA6OiBOYXR1cmFsIG4gPT4gW2FdIC0+IFYgbiBhCmJhZF9mcm9tTGlzdCBsID0gaWYgbGVuZ3RoIGwgPT0gZGltJ1YgdiB0aGVuIHYgZWxzZSB1bmRlZmluZWQgLS0gdGhpcyBpcyBsaW5lIDExCiAgd2hlcmUgdiA9IFZfIGwKCgpiYWRfZiA6OiBOYXR1cmFsIG4gPT4gW2FdIC0+IChWIG4gYSwgSW50KQpiYWRfZiB4cyA9ICh2LCBkaW0nViB2KQogIHdoZXJlIHYgPSBWXyB4cwoKZ29vZF9mIDo6IE5hdHVyYWwgbiA9PiBhIC0+IChWIG4gYSwgSW50KQpnb29kX2YgeCA9ICh2LCBkaW0nViB2KQogIHdoZXJlIHYgPSBWXyAkIHJlcGxpY2F0ZSAoZGltJ1YgdikgeAoKCmZyb21MaXN0J1YgOjogZm9yYWxsIG4gYS4gTmF0dXJhbCBuID0+IFthXSAtPiBWIG4gYQpmcm9tTGlzdCdWIGwgPSBhc3NlcnQgKGxlbmd0aCBsID09IGRpbSdWIHYpIHYKICB3aGVyZSB2ID0gVl8gbCAgLS0gOjogViBuIGEgLS0gd2h5IGNhbid0IEdIQyBpbmZlciB0aGlzIHR5cGU/CgppbnN0YW5jZSBOYXR1cmFsIG4gPT4gQXBwbGljYXRpdmUgKFYgbikgd2hlcmUKICBwdXJlIHggPSB2CiAgICB3aGVyZSAgdiA9IFZfICQgcmVwbGljYXRlIChkaW0nViB2KSB4IC0tIEdIQyBpbmZlcnMgdGhpcyB0eXBlCiAgKFZfIGZzKSA8Kj4gKFZfIHhzKSA9IFZfICQgemlwV2l0aEV4YWN0ICgkKSBmcyB4cwoKCnppcFdpdGhFeGFjdCA6OiAoYSAtPiBiIC0+IGMpIC0+IFthXSAtPiBbYl0gLT4gW2NdIAp6aXBXaXRoRXhhY3QgXyBbXSBbXSA9IFtdCnppcFdpdGhFeGFjdCBmICh4OnhzKSAoeTp5cykgPSBmIHggeSA6IHppcFdpdGhFeGFjdCBmIHhzIHlzIAp6aXBXaXRoRXhhY3QgXyBfIF8gPSBlcnJvciAiemlwV2l0aEV4YWN0OiBsZW5ndGggbWlzbWF0Y2giIAo=
[1 of 1] Compiling Vec ( prog.hs, prog.o )
Warning: output was redirected with -o, but no output will be generated
because there is no Main module.