Strange type behavior with GADT type (for fixed length vectors)

Question

I have the following gadt

data Vec na where T :: Vec VZero a (:.) :: (VNat n) => a -> (Vec na) -> (Vec (VSucc n) a) 

for modeling fixed-length vectors using the class

 class VNat n data VZero instance VNat VZero data VSucc n instance (VNat n) => VNat (VSucc n) 

I tried to program the append function on vectors:

 vAppend :: Vec nb -> Vec mb -> Vec nm b vAppend TT = T -- nonsense, -- its just a minimal def for testing purposes 

Type check do not like:

  Could not deduce (nm ~ VZero) from the context (n ~ VZero) bound by a pattern with constructor T :: forall a. Vec VZero a, in an equation for `vAppend' at VArrow.hs:20:9 or from (m ~ VZero) bound by a pattern with constructor T :: forall a. Vec VZero a, in an equation for `vAppend' at VArrow.hs:20:11 `nm' is a rigid type variable bound by the type signature for vAppend :: Vec nb -> Vec mb -> Vec nm b at VArrow.hs:20:1 Expected type: Vec nm b Actual type: Vec VZero b In the expression: T In an equation for `vAppend': vAppend TT = T Failed, modules loaded: Vectors. 

Can someone explain the problems of GHC with a variable like nm ? And what exactly does ~ mean in the error message?

Answer 1

Be that as it may, you say that you can get a vector of any length by adding two vectors. If you cancel the ghc signature, it means that vAppend should give a VZero length vector taking into account any two vectors - this makes sense, but not what you want. You need the Plus type associated with your VNat to restrict the type of vAppend result to vectors. A natural way would be some type family, but I could not get it under the VNat class. In any case, this whole idea is much clearer with the advanced DataKinds extension DataKinds (in ghc-7.4 and later) - although, perhaps, you deliberately tried to avoid this extension? This eliminates the annoying unclosed VSucc character that VSucc Char allows, etc. If you have not tried to avoid DataKinds , then your module might look something like this:

 {-#LANGUAGE GADTs, TypeFamilies, DataKinds, TypeOperators#-} data Vec na where -- or: data Vec :: VNat -> * -> * where T :: Vec VZero a (:.) :: a -> Vec na -> Vec (VSucc n) a -- no class constraint data VNat = VZero | VSucc VNat -- standard naturals type family n :+ m :: VNat -- note the kind of a ":+" is a promoted VNat type instance VZero :+ n = n type instance VSucc n :+ m = VSucc (n :+ m) vAppend :: Vec nb -> Vec mb -> Vec (n :+ m) b vAppend T v = v vAppend (a :. u) v = a :. (vAppend uv) 

Edit: it seems to me that the string for the Plus family - or :+ should explicitly limit the types of arguments

 type family (n::VNat) :+ (m::VNat) :: VNat 

to save garbage types such as Char :+ VZero , etc., that is, according to the same principle that DataKinds preferred for data VSucc n types of type data VSucc n . In addition, we can see that these two instances fully define it, although I do not know how much to use the compiler for this.

Answer 2

All type variables in a type signature are universally evaluated. This means that if you say that the function is of type

 Vec nb -> Vec mb -> Vec nm b 

then for any choice of n , m , nm and b this type must be valid. In particular, for example,

 Vec VZero Int -> Vec VZero Int -> Vec (VSucc VZero) Int 

must also be a valid type of your function. However, the addition of two vectors does not have this general type. There are restrictions on nm , namely: nm is the sum of numbers of type n and m . You must express these restrictions in the type of the function, otherwise you will get type errors.

In your case, GHC complains that your definition of nm is actually VZero , so you make assumptions about nm that your type indicates what you are forbidden to do. ~ is just a GHC symbol for type equality.

Answer 3

When writing a function by matching patterns by values ​​GADT GHC uses information about the expected behavior during the execution of your function when checking each sentence. Your vAppend function has only one sentence, this template corresponds to a value of type Vec nb and another value of type Vec mb . The GHC explains that if, at run time, vAppend is applied to actual arguments that match the T pattern, then the actual type of the actual arguments should be Vec VZero b , which is more informative than just Vec nb or Vec mb . The way this reasoning is implemented in the GHC is that when checking the RHS type of the unique vAppend it fixes the assumption that n must be really VZero , n ~ VZero , as well as m ~ VZero .

The type you write for the function sets up the contract that it must execute. The error message you receive is related to the fact that the contract that must be executed when implementing vAppend is too general. You say that, given two vectors of length n and m , vAppend should create a vector that can be considered any size. Indeed, the GHC notices that your implementation does not fulfill this contract, because the type of your RHS Vec VZero b does not match the expected type of RHS, Vec nm b , and there is no assumption that nm ~ VZero . Indeed, the only assumptions available to us, says the GHC, are those from the previous paragraph.

The only possible way to fulfill this contract is to write undefined as the RHS of your proposal. This is clearly not what you want. The trick to getting the right type for vAppend is to somehow relate the size of the output vector to the corresponding size of the two input vectors. It might look like this:

 type family Plus nm type instance Plus VZero m = m type instance Plus (VSucc n) m = VSucc (Plus nm) vAppend :: Vec nb -> Vec mb -> Vec (Plus nm) b vAppend TT = T 

We said here that the length is determined by the lengths of the inputs before vAppend , through some function on types called Plus . In the case where both VZero input VZero , we know that Plus nm same as Plus VZero VZero , since n ~ VZero and m ~ VZero . Since Plus VZero VZero is in the form of an instance of the first type family, GHC knows that it matches VZero . Therefore, in this thread, the GHC expects RHS like Vec VZero b , which we can easily build!