You miss apprehend.  I'm saying that the first class modules encoding in that paper is expressible using a subset of ghc core. <div><br></div><div>There IS the subtle issue that type class dictionaries / type classes have different sharing and strictness semantics than normal userland records. </div><div><br></div><div>There's a space Of designs that could provide what you're asking for, and I do agree that it's worth exploring. I guess The main question is whether or not it turns into its own research engineering project. </div><div><br></div><div>Likewise, to what extent aside from syntactic nicety does implicit parameters and the punning extensions not suffice?<span></span><br><br>On Saturday, April 25, 2015, Ertugrul Söylemez <<a href="mailto:ertesx@gmx.de">ertesx@gmx.de</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">> Isn't your associated type here more like a dependent record field/<br>
> existential that we can kinda expose?<br>
<br>
Not quite.  There is still a clear distinction between type and value<br>
level.  You cannot refer to an AT on the value level or to a member<br>
value on the type level.<br>
<br>
<br>
> This does seem to veer into first class module territory.  Especially<br>
> wrt needing first class types in a fashion.<br>
<br>
I think formally there is little difference between a powerful record<br>
system and a first-class module system.  However, even in a<br>
non-dependent language a first class module could still expect a value<br>
argument.  A record type couldn't do this without essentially making the<br>
language dependent on the way.<br>
<br>
<br>
> Have you had a chance to peruse the Andreas Rossberg 1ml paper on<br>
> embedding first class modules into f omega that has been circulating?<br>
> Perhaps there are ideas There that could be adapted. Especially since<br>
> core is an augmented f omega<br>
<br>
I haven't read it, sorry.  My proposal should conform to the current<br>
core language, as it's mostly just a syntax transformation.  The only<br>
new semantics would be defaults.<br>
</blockquote></div>