Databases
StackOverflow2013
Postsdbo
PO
 

Note that there are some explanatory texts on larger screens.

plurals
  1. PO
    primarykey
    data
    text
    <p>When writing a function by pattern matching on values of a GADT, GHC uses information about the expected behaviour at runtime of your function when type checking each clause. Your <code>vAppend</code> function has only one clause, that pattern matches a value of type <code>Vec n b</code> and a another value of type <code>Vec m b</code>. GHC reasons that if at runtime <code>vAppend</code> is applied to actual arguments that both match against the pattern <code>T</code>, then the actual type of the actual arguments must be of the form <code>Vec VZero b</code>, which is a more informative type than just <code>Vec n b</code> or <code>Vec m b</code>. The way this reasoning is implemented in GHC is that when type checking the RHS of the unique clause of <code>vAppend</code>, it records an assumption that <code>n</code> must surely actually be <code>VZero</code>, written <code>n ~ VZero</code>, and likewise <code>m ~ VZero</code>.</p> <p>The type you write for a function sets out the contract that it must fulfill. The error message that you are getting is because the contract that must be fulfilled by the implementation of <code>vAppend</code> is much too general. You are saying that given two vectors of some lengths <code>n</code> and <code>m</code>, <code>vAppend</code> must produce a vector that can be considered to be of <em>any</em> size. Indeed, GHC notices that your implementation does not fulfill this contract, because the type of your RHS, <code>Vec VZero b</code>, does not match the expected type of the RHS, <code>Vec nm b</code>, and there is no assumption saying the <code>nm ~ VZero</code>. Indeed the only assumptions available, GHC tells us, are the ones from the previous paragraph.</p> <p>The only possible way you could fulfill this contract is by writing <code>undefined</code> as the RHS of your clause. That is obviously not what you want. The trick to getting the type right for <code>vAppend</code> is to somehow relate the size of the output vector to the respective size of the two input vectors. That might go like this:</p> <pre><code>type family Plus n m type instance Plus VZero m = m type instance Plus (VSucc n) m = VSucc (Plus n m) vAppend :: Vec n b -&gt; Vec m b -&gt; Vec (Plus n m) b vAppend T T = T </code></pre> <p>What we have done here is said that that the length is determined by the lengths of the inputs to <code>vAppend</code>, through some function on types called <code>Plus</code>. In the case where both input lengths are <code>VZero</code>, then we know that <code>Plus n m</code> is the same as <code>Plus VZero VZero</code> since <code>n ~ VZero</code> and <code>m ~ VZero</code>. Since <code>Plus VZero VZero</code> is of the shape of the first type family instance, GHC knows that it is the same as <code>VZero</code>. Therefore in this branch GHC expects a RHS of type <code>Vec VZero b</code>, which we can readily construct!</p>
    singulars
    1. This table or related slice is empty.
    1. POStrange type inference behaviour with GADT type (for fixed length vectors)
      singulars
      1. PTQuestion
    1. PTAnswer
    1. This table or related slice is empty.
    1. USmacron
    plurals
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. This table or related slice is empty.
    1. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    2. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    3. VO
      singulars
      1. PO
      1. This table or related slice is empty.
      1. VTUpMod
    1. COThanks, very helpful answer! Unfortunately, it doesnt work with a real world function body like: `vAppend T v = v` and/or `vAppend (x :. xs) v = x :. (vAppend xs v)`. Maybe, you have a neat solution for those cases?
      singulars
      1. PO
      1. USphynfo
    2. COHm, the problem there is that there is no way to tell GHC that `VNat` is closed under addition - that is, that if `VNat n` and `VNat m`, then we should also have `VNat (Plus n m)`. GHC doesn't let us add the appropriate instance, so it looks like you'll have to use the `DataKinds` extension for this one, as explained by applicative. I guess that's a separate issue from the one you are concerned with in your original question, though, which was about why GHC complained given the type signature you wrote.
      singulars
      1. PO
      1. USmacron
 

Querying!

 
Guidance
A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload