fork download
  1. {-# LANGUAGE ScopedTypeVariables, DeriveTraversable
  2. , DeriveFunctor, DeriveFoldable, MonoLocalBinds #-}
  3.  
  4. {-# OPTIONS_GHC -Wall #-}
  5.  
  6. module Vec where
  7.  
  8. import Control.Exception.Base (assert)
  9. import Data.Proxy
  10. import Control.Applicative
  11. import Data.Foldable
  12. import Data.Traversable
  13.  
  14. -- Peano numbers
  15. data N0
  16. data Succ n
  17.  
  18. type N1 = Succ N0
  19. type N2 = Succ N1
  20. type N3 = Succ N2
  21. type N4 = Succ N3
  22.  
  23. naturalPred :: Proxy (Succ n) -> Proxy n
  24. naturalPred _ = Proxy
  25.  
  26. class Natural n where
  27. fromNatural :: Proxy n -> Int
  28.  
  29. instance Natural N0 where
  30. fromNatural _ = 0
  31.  
  32. instance Natural n => Natural (Succ n) where
  33. fromNatural n = fromNatural (naturalPred n) + 1
  34.  
  35. -- fixed length lists
  36. -- I'll only need lists of length up to 4
  37.  
  38. newtype V n a = V_ { get'V :: [a] }
  39. deriving (Show, Eq, Ord, Functor, Foldable, Traversable)
  40.  
  41. dim'V :: forall n a. Natural n => V n a -> Int
  42. dim'V _ = fromNatural (Proxy :: Proxy n)
  43.  
  44.  
  45. bad_fromList :: Natural n => [a] -> V n a
  46. bad_fromList l = if length l == dim'V v then v else undefined -- this is line 11
  47. where v = V_ l
  48.  
  49.  
  50. bad_f :: Natural n => [a] -> (V n a, Int)
  51. bad_f xs = (v, dim'V v)
  52. where v = V_ xs
  53.  
  54. good_f :: Natural n => a -> (V n a, Int)
  55. good_f x = (v, dim'V v)
  56. where v = V_ $ replicate (dim'V v) x
  57.  
  58.  
  59. fromList'V :: forall n a. Natural n => [a] -> V n a
  60. fromList'V l = assert (length l == dim'V v) v
  61. where v = V_ l -- :: V n a -- why can't GHC infer this type?
  62.  
  63. instance Natural n => Applicative (V n) where
  64. pure x = v
  65. where v = V_ $ replicate (dim'V v) x -- GHC infers this type
  66. (V_ fs) <*> (V_ xs) = V_ $ zipWithExact ($) fs xs
  67.  
  68.  
  69. zipWithExact :: (a -> b -> c) -> [a] -> [b] -> [c]
  70. zipWithExact _ [] [] = []
  71. zipWithExact f (x:xs) (y:ys) = f x y : zipWithExact f xs ys
  72. zipWithExact _ _ _ = error "zipWithExact: length mismatch"
  73.  
Compilation error #stdin compilation error #stdout 0s 0KB
stdin
Standard input is empty
compilation info
[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.
stdout
Standard output is empty