<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">Yes -- apologies for not posting to this list last night, but I was eager to get my proposal out the door while it was topical... and then eager to get to bed once it had. That proposal (<a href="https://github.com/ghc-proposals/ghc-proposals/pull/378" class="">https://github.com/ghc-proposals/ghc-proposals/pull/378</a>) is, in a sense, a generalization of this thread (thanks, Arnaud for starting it).<div class=""><br class=""></div><div class="">To Iavor's email: I think the design you describe makes good sense, but only for a language without dependent types. A language with dependent types could be imagined with "languages above" and "languages below", but I think the "above"/"below" switching would introduce friction with little self-sustaining benefit. By "self-sustaining" there, I mean that a dependently typed language often has no need for different languages above or below, and so making that distinction in a dependently typed language is awkward. However, one could imagine a dependently typed Haskell that retains the distinction, essentially for philosophical backward compatibility. ("Philosophical" because I believe we can design dependent types in Haskell to be fully backward compatible, but it might require a new way of thinking about what phrases in the language mean.)</div><div class=""><br class=""></div><div class="">Perhaps even more directly, avoiding a distinction between languages above/below is a key component of what I require in an ergonomic interpretation of dependent types. Keeping the distinction would, unless I'm convinced otherwise, appear un-ergonomic.</div><div class=""><br class=""></div><div class="">Richard<br class=""><div class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Nov 14, 2020, at 7:21 AM, Alejandro Serrano Mena <<a href="mailto:trupill@gmail.com" class="">trupill@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div class="">
<div dir="ltr" class="">
This might be relevant to this discussion. Richard Eisenberg has opened a proposal to give a “general steering” towards Dependent Haskell, or not.</div><div dir="ltr" class="">- Proposal: <a href="https://github.com/ghc-proposals/ghc-proposals/pull/378" class="">https://github.com/ghc-proposals/ghc-proposals/pull/378</a></div><div dir="ltr" class="">- Reddit: <a href="https://www.reddit.com/r/haskell/comments/jtvf06/should_ghc_support_ergonomic_dependent_types/" class="">https://www.reddit.com/r/haskell/comments/jtvf06/should_ghc_support_ergonomic_dependent_types/</a></div><div dir="ltr" class=""><br class=""></div><div dir="ltr" class="">I think it’s also a place where we all should express our opinion.</div><div dir="ltr" class=""><br class=""></div><div dir="ltr" class="">Alejandro</div><div dir="ltr" class=""><br class="">
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On 13 Nov 2020 at 16:51:58, Iavor Diatchki <<a href="mailto:iavor.diatchki@gmail.com" class="">iavor.diatchki@gmail.com</a>> wrote:<br class=""></div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div class="">
_______________________________________________<br class="">ghc-steering-committee mailing list<br class=""><a href="mailto:ghc-steering-committee@haskell.org" class="">ghc-steering-committee@haskell.org</a><br class=""><a href="https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee" class="">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee</a><br class="">
</div>
</blockquote>
</div>
</div>
</div>
_______________________________________________<br class="">ghc-steering-committee mailing list<br class=""><a href="mailto:ghc-steering-committee@haskell.org" class="">ghc-steering-committee@haskell.org</a><br class="">https://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-steering-committee<br class=""></div></blockquote></div><br class=""></div></div></body></html>