[Haskell-cafe] Selda: confused about type signtures
marc at lamarciana.com
Mon Apr 23 18:08:18 UTC 2018
Tom, thank you very much for your deep inspection. Your gist can be
really helpful in trying to understand the problem. I will study it
carefully. I have been reading books about Haskell and also Category
Theory for some months, but I have just started coding few weeks ago, so
I'm bit overwhelmed about having found a compiler bug so soon :D I'll
look into all of this and also about Li-yao recommendations and if it is
suitable I'll fill the issue and also report here.
On Mon, 23 Apr 2018, Tom Ellis wrote:
> On Mon, Apr 23, 2018 at 04:54:36PM +0200, Marc Busqué wrote:
>> On Mon, 23 Apr 2018, Tom Ellis wrote:
>> >I had an error in what I said and also it was imprecise. It's
>> >`Res (Cols s a)` which is `a`, but only in the cases where you're actually
>> >going to use it, and the compiler cannot take that into account when
>> >solving the constraint. Anyway, as Li-yao Xia points out in a sibling
>> >message, the type variable `s` in not constrained and therefore it seems
>> >impossible to solve.
>> I have pushed the repo to Github:
> Thanks for that Marc, it's very helpful. I extracted the parts that are
> relevant to the problem and created a version that doesn't depend on Selda:
> I think I now understand what the situation is. Interestingly your code
> works on 8.0 but not 7.10.
> Contrary to my earlier presumptions, the compiler *is* able to give a type
> to `list` because `Cols` is a closed type family. I suppose it can
> determine that `Cols s a` does not actually depend on `s` so giving list the
> (Result (Cols s a), Columns (Cols s a)) => Table a -> Res (Cols s a)
> is fine. The type of `s` will never be needed. When `list` is applied to
> `categories` then `a` is fixed and `Res (Cols s a)` is fixed, regardless of
> what `s` is.
> Subtly changing the definition of Cols will break things. For example, if
> you add the clause
> Cols () a = Col Int a
> then you won't be able to define `list` any more, even though `Res (Cols s
> a)` is still just `a` because the `Columns (Cols s a)` instance might then
> depend on what `s` is.
> On the other hand, I do not yet understand why you cannot provide an
> explicit signature for `list`. I suspect this is some hairy compiler bug.
> Either it should be possible to give `list` its inferred type or it should
> be forbidden. It's probably worth filing an issue about this on GHC Trac.
> I would be interested to hear Li-yao's thoughts on the matter.
> Incidentally, this is why I try to avoid type families as much as possible.
> When they go wrong it's very hard to understand why, and indeed when they go
> right it's also very hard to understand why.
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> Only members subscribed via the mailman list are allowed to post.
More information about the Haskell-Cafe