Here's the paper you're looking for:
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/scopedlabels.pdf

I believe it's fully decidable. Elm is basically Damas Milner plus these
records, so it stays decidable.

It's usually called row polymorphism, and isn't really subtyping, although
you get something like subtyping if you combine it with existential types,
which would lose decidability.

On Feb 10, 2017 6:30 AM, "'Rupert Smith' via Elm Discuss" <
elm-discuss@googlegroups.com> wrote:

> For my undergraduate project (20+ years ago), I implemented a language
> called Ob<: (or ObSub) from "A Theory of Objects" by Abadi and Cardelli.
> This language is related to the functional language F<: (functional
> calculus with sub-typing), which is somewhat related to F#. My project
> supervisor worked for Microsoft Research and was involved in the .Net
> project.
>
> One thing about Ob<: is that due to the sub-typing relation in the
> language, typing became semi-decideable. Given a type and a program, you
> can decide if the program fits the type (checking), but given a program you
> cannot work out what its type is (inference). This meant that you had to
> give the type in full of every program you wrote - sometimes the type was
> longer than the program!
>
> As I understand it, Elm uses a different extensible record type to that of
> OO languages with full-blown sub-typing? Does anyone have a reference to
> the paper this is based on?
>
> And am I right in thinking that this version of extensible records is
> fully decideable and all types can always be infered?
>
> I am just trying to understand what exactle extensible records are and
> what their limitations are. As far as I can tell, sub-typing cannot really
> be represented in Elm - the concrete type of something must be known fully
> in advance? Makes sense I suppose, there is no dynamic loading and linking
> of code at runtime, and allowing it would need runtime type checks (uuughh).
>
> ========
>
> I added this example here to one of the compiler issues:
>
> https://github.com/elm-lang/elm-compiler/issues/1504
>
> type alias Record1 =
>     { field : String, otherField : String }
>
>
> type alias Record2 =
>     { otherField : String }
>
>
> type Grouping
>     = R1 Record1
>     | R2 Record2
>
>
> extract : (a -> String) -> Grouping -> String
> extract selector grouping =
>     case grouping of
>         R1 record ->
>             selector record
>
>         R2 record ->
>             selector record
>
> What I am trying to do here is to write a general function that will let
> me select a field from a record type out of a choice of several different
> record types. I also tried recently to reformulate this using extensible
> records but just ended up in a mess.
>
> This came about because I was trying to map a data model which on the
> server side in Java does use sub-typing. I suspect that what I need in
> order to be able to extract an arbitrary field at runtime from a set of
> fields is to use a Dict...
>
> --
> You received this message because you are subscribed to the Google Groups
> "Elm Discuss" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to elm-discuss+unsubscr...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

-- 
You received this message because you are subscribed to the Google Groups "Elm 
Discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to elm-discuss+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Reply via email to