I'm not aware of any arguments against them, though I'm not aware of them being proposed before either. My knowledge of the dependent types literature is sparse, but from what I've seen, most of it is dashing headlong into full dependent types and trying to solve the problems that come with it. I've found considerably less on exploring the design space to say what pieces are tractable in isolation or where exactly it all starts to break down.
It's particularly funny that I came back to this old idea now and ranted about it, because the next day (last night) when working on the ICFP programming contest (http://www.icfpcontest.org/) I really wanted them so that I could implement the type for the incoming messages appropriately, i.e. as a union of record types (which GHC permits, but it isn't type-safe about the field accessors (i.e. you can call the accessors on any branch of the union, even if the other branches lack such a field)).
If I can get the free time to start hacking on GHC (ha!) or if I can convince my advisor that improving GHC will help for Dyna (ha! but maybe marginally less so) then I might see about implementing them myself and writing a couple papers on it. Right now types and type constructors are in a different namespace than functions and data constructors, with difference types we would still be making that distinction though how we discuss it needs to change[1] and how to reconcile that still needs to be worked out, along with some details about how they interact with the records syntax.
[1] Since the token Just could be either a type- or data-constructor now, depending on whether it's in a type context or an expression context.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
chiming
no subject
Date: 2008-07-13 06:37 am (UTC)From:It's particularly funny that I came back to this old idea now and ranted about it, because the next day (last night) when working on the ICFP programming contest (http://www.icfpcontest.org/) I really wanted them so that I could implement the type for the incoming messages appropriately, i.e. as a union of record types (which GHC permits, but it isn't type-safe about the field accessors (i.e. you can call the accessors on any branch of the union, even if the other branches lack such a field)).
If I can get the free time to start hacking on GHC (ha!) or if I can convince my advisor that improving GHC will help for Dyna (ha! but maybe marginally less so) then I might see about implementing them myself and writing a couple papers on it. Right now types and type constructors are in a different namespace than functions and data constructors, with difference types we would still be making that distinction though how we discuss it needs to change[1] and how to reconcile that still needs to be worked out, along with some details about how they interact with the records syntax.
[1] Since the token
Justcould be either a type- or data-constructor now, depending on whether it's in a type context or an expression context.