[PL-sem-jr] Impredicatives vs. higher-ranks

[Artem Pelenitsyn]

Hey, Daniel!

Thank you for your feedback, it is appreciated.

You see, some time left since I posted this question; I forget some things
which pushed me to ask it. I probably could search the actual code over my
computer but don't feel it worth.

In short, I saw two parts of your point. One on isomorphism. I don't get
that point even when it rose at SO. I do have some algebra and categories
over me. The isomorphism between two types A, B (constructively) arise when
you have two morphisms: A -> B and B -> A, but I have just one (A ->
Showable), not the other one. I also cannot follow the downcasting talks:
if I have heterogeneous list, I can pass it to a function, which treats the
list as a list of showables, back to caller I can continue to work with my
list, not loosing any type information.

The second part with possible solutions leaves a couple of questions, but
from code that you gave, I don't see substantial improvement over
-XExistentialQuantification-approach presented in the initial SO post.

Surprisingly some of people over SO tried to convenience me that I want to
do strange thing. But I cannot see what's wrong with the type [forall a.
Show a => a]. I guess that it is some GHC's internal problems which prevent
the actual implementation of -XImpredicativeTypes. And that's it. If I had
it, I wouldn't hit a problem.

-- Artem



вт, 24 янв. 2017 г. в 15:31, Daniel Patterson <dbp at dbpmail.net>:

> It may be a good example to talk about existentials, rank-n, etc, but as a
> task in itself, it's somewhat a solution looking for a problem - as soon as
> you existentially quantify (which is what you are doing, regardless of the
> mechanism), as some of the commenters pointed out, your data is isomorphic
> to String - or to any fixed interface of functions.
>
> Since there is no type reflection or downcast in Haskell, the extra data
> (beyond the interface) is irrelevant, and you might as well store the
> operations in the list rather than the original data. e.g., in the general
> case:
>
> data Op = unOp { op1 :: Res1, op2 :: Res2, ..., opn ::  Resn }
> class OpInterface a where
>   toOp a :: Op
>
> So the type you are writing is just `[Op]`.
>
> You then implement the interface for the types you care about, and then
> put `toOp mydata` when adding to the list. When you pull things out of the
> list you call `op1.unOp` or `op2.unOp` on them, which is the only thing you
> would be permitted even in the more complicated case using existentials. I
> guess you could complain that you have to write `toOp`, rather than having
> it implicitly inserted for you, and that you have to write `opn.unOp`
> rather than just `opn`, but I think that says more about Haskell's design
> methodology than anything fundamental - I believe Scala will automatically
> insert calls to coerce between types if you have the right stuff set up.
>
> Why this works is essentially the connection between closures and
> existentials - from Minimide, Morrisett, Harper 95 (
> https://www.cs.cmu.edu/~rwh/papers/closures/tr.pdf) - that closures
> implicitly existentially quantify over their free variables, which in this
> case are the heterogeneous pieces of data. So in the above example, you
> have a homogenous list of Op's, but different ones are closing over pieces
> of data of different types, all of which implement the OpInterface, of
> course.
>
> On Tue, Jan 24, 2017 at 3:06 PM Artem Pelenitsyn <
> artem.pelenitsyn at gmail.com> wrote:
>
> Just in case: really simple task hardly solved in Haskell (my SO
> question), which mentions all bloody mess mentioned today (Impreds, Higher
> Rank, Existensials):
>
> http://stackoverflow.com/q/33586720/465100
>
> The distinction of Higher-Ranked and Impredicatives basically: you can
> have foralls only inside `->` type operator in the former and in *any*
> type operator (e.g. lists) in the latter.
>
> --
> best wishes,
> Artem
>
> _______________________________________________
> Pl-sem-jr mailing list
> Pl-sem-jr at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-sem-jr
>
>
-------------- next part --------------
HTML attachment scrubbed and removed