(bound at /home/matt/Projects/dep-types.hs:32:17) Xs :: Vector m a (bound at /home/matt/Projects/dep-types.hs:32:23) In the expression: VCons a (append rest xs)Īppend (VCons a rest) xs = VCons a (append rest xs).Could not deduce: Add n1 ('Succ m) ~ 'Succ (Add n1 m)Īt /home/matt/Projects/dep-types.hs:32:9-20.home/matt/Projects/dep-types.hs:32:28: error:
Compiling DepTypes ( /home/matt/Projects/dep-types.hs, interpreted ) Let’s replace the definition we have thus far with undefined, reload in GHCi, and inspect some types: It knows that n (the length of the first parameter) is Zero because we’ve pattern matched on VNil. GHC is telling us that it can’t infer that m (which is the length of the second parameter vector) is equal to Zero. The error is kinda big and scary at first. (bound at /home/matt/Projects/dep-types.hs:31:1) (bound at /home/matt/Projects/dep-types.hs:31:13)Īppend :: Vector n a -> Vector m a -> Vector (Add n m) a In an equation for ‘append’: append VNil rest = VNil Vector n a -> Vector m a -> Vector (Add n m) aĪt /home/matt/Projects/dep-types.hs:30:11 So I’m seeing that we’re passing types to Maybe, in much the same way that we pass values to MkIntAndChar.Īt /home/matt/Projects/dep-types.hs:31:8-11Īppend :: forall (n :: Nat) a (m :: Nat). I am a value of Maybe a, for any and all types a that you might provide to me. The reason is that nothingA :: Maybe a really means: That makes sense – (=) only works on values that have the same type.īut then, wait, why does nothingA not complain when compared with nothingInt and nothingChar? Woah – we get a type error when trying to compare nothingInt with nothingChar. Monads provide a way to structure a program. Monads are abstract, and they have many useful concrete instances. In the second argument of ‘ ( = ) ’, namely ‘ nothingChar ’ In the expression : nothingInt = nothingChar In an equation for ‘ it ’ : it = nothingInt = nothingChar λ > nothingA = nothingInt True λ > nothingA = nothingChar True A monad is an algebraic structure in category theory, and in Haskell it is used to describe computations as sequences of steps, and to handle side effects such as state and IO.Couldn't match type ‘ Char ’ with ‘ Int ’ Expected type : Maybe Int Actual type : Maybe Char.Λ > let nothingA = Nothing :: Maybe a λ > let nothingInt = Nothing :: Maybe Int λ > let nothingChar = Nothing :: Maybe Char λ > nothingInt = nothingChar \: 27 : 15 : error :
0 kommentar(er)
