<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Aug 11, 2018, at 11:27 AM, Vassil Ognyanov Keremidchiev <<a href="mailto:varosi@gmail.com" class="">varosi@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><span style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; float: none; display: inline !important;" class="">What are the new features there toward Dependent Typed Haskell?</span></div></blockquote></div><br class=""><div class="">Ben's link to <a href="https://downloads.haskell.org/~ghc/8.6.1-beta1/docs/html/users_guide/8.6.1-notes.html" class="">https://downloads.haskell.org/~ghc/8.6.1-beta1/docs/html/users_guide/8.6.1-notes.html</a> includes several items, pasted here:</div><div class=""><br class=""></div><div class="">* A new <a class="internal reference" href="https://downloads.haskell.org/~ghc/8.6.1-beta1/docs/html/users_guide/glasgow_exts.html#extension-StarIsType"><tt class="literal std-extension docutils xref std">StarIsType</tt></a> language extension has been added which controls

whether <tt class="literal docutils">*</tt> is parsed as <tt class="literal docutils">Data.Kind.Type</tt> or a regular type operator.

<a class="internal reference" href="https://downloads.haskell.org/~ghc/8.6.1-beta1/docs/html/users_guide/glasgow_exts.html#extension-StarIsType"><tt class="literal std-extension docutils xref std">StarIsType</tt></a> is enabled by default.</div><div class=""><br class=""></div><div class="">* CUSKs now require all kind variables to be explicitly quantified. This was

already the case with <a class="internal reference" href="https://downloads.haskell.org/~ghc/8.6.1-beta1/docs/html/users_guide/glasgow_exts.html#extension-TypeInType"><tt class="literal std-extension docutils xref std">TypeInType</tt></a>, but now <a class="internal reference" href="https://downloads.haskell.org/~ghc/8.6.1-beta1/docs/html/users_guide/glasgow_exts.html#extension-PolyKinds"><tt class="literal std-extension docutils xref std">PolyKinds</tt></a>

also exhibits this behavior.</div><div class=""><br class=""></div><div class="">* Functionality of <a class="internal reference" href="https://downloads.haskell.org/~ghc/8.6.1-beta1/docs/html/users_guide/glasgow_exts.html#extension-TypeInType"><tt class="literal std-extension docutils xref std">TypeInType</tt></a> has been subsumed by

<a class="internal reference" href="https://downloads.haskell.org/~ghc/8.6.1-beta1/docs/html/users_guide/glasgow_exts.html#extension-PolyKinds"><tt class="literal std-extension docutils xref std">PolyKinds</tt></a>, and it is now merely a shorthand for

<a class="internal reference" href="https://downloads.haskell.org/~ghc/8.6.1-beta1/docs/html/users_guide/glasgow_exts.html#extension-PolyKinds"><tt class="literal std-extension docutils xref std">PolyKinds</tt></a>, <a class="internal reference" href="https://downloads.haskell.org/~ghc/8.6.1-beta1/docs/html/users_guide/glasgow_exts.html#extension-DataKinds"><tt class="literal std-extension docutils xref std">DataKinds</tt></a>, and <a class="internal reference" href="https://downloads.haskell.org/~ghc/8.6.1-beta1/docs/html/users_guide/glasgow_exts.html#extension-StarIsType"><tt class="literal std-extension docutils xref std">NoStarIsType</tt></a>.

The users are advised to avoid <a class="internal reference" href="https://downloads.haskell.org/~ghc/8.6.1-beta1/docs/html/users_guide/glasgow_exts.html#extension-TypeInType"><tt class="literal std-extension docutils xref std">TypeInType</tt></a> due to its misleading

name: the <tt class="literal docutils"><span class="pre">Type</span> <span class="pre">::</span> <span class="pre">Type</span></tt> axiom holds regardless of whether it is enabled.</div><div class=""><br class=""></div><div class="">These are small steps, to be sure, but there's quite a bit going on behind the scenes. For example see the "Coercion Quantification" and "Type-level visible type applications" to take place at HIW (<a href="https://icfp18.sigplan.org/track/hiw-2018-papers#event-overview" class="">https://icfp18.sigplan.org/track/hiw-2018-papers#event-overview</a>).</div><div class=""><br class=""></div><div class="">There are also a great many proposals in play at <a href="https://github.com/ghc-proposals/ghc-proposals" class="">https://github.com/ghc-proposals/ghc-proposals</a></div><div class=""><br class=""></div><div class="">More to come in the future, of course!</div><div class="">Richard</div></body></html>