Types

Post by thinkpad20 » Thu, Aug 25, 2016, 3:30 PM UTC

seanwilson wrote: post #162

thinkpad20 wrote: post #108

Earlier quoted context omitted.

> Sure, but my point is that any nontrivial property requires the programmer to write difficult formal mathematical proofs which is an activity completely unlike what you see in mainstream strongly typed languages (e.g. Haskell, OCaml). So don't write the proofs then. Dependently typed languages don't require you to write proofs; they give you the ability to if you choose. Considering that it's impossible to write su…

> Considering that it's impossible to write such proofs in OCaml or Haskell, it seems strange to complain that they're hard to write in a dependently typed language. My sole point is that when I see articles on here about dependently typed languages, the issue of how the proofs are generated and the challenges involved in doing this is overlooked almost every time. I think it's important these challenges are highligh…

Post by dragonwriter » Thu, Aug 25, 2016, 3:51 PM UTC

catnaroek wrote: post #182

dragonwriter wrote: post #180

Earlier quoted context omitted.

If classes are types, subsclasses should be subtypes -- so the above restrictions should just be applied to subclass relationships. One could also have an non-subclassing mechanism of implementation sharing, that might be declared something like this: class Related does (method1, method2) like Base; or class Related does all except (method3) like Base;

That syntax is too heavyweight (IMO). AFAICT, most of the time, when people use inheritance, they don't want to define perfect subtypes. They just want to reuse as much already implemented behavior as possible.

  class Related like Base;

Post by [deleted] » Thu, Aug 25, 2016, 4:36 PM UTC

dragonwriter wrote: post #183

catnaroek wrote: post #182

Earlier quoted context omitted.

That syntax is too heavyweight (IMO). AFAICT, most of the time, when people use inheritance, they don't want to define perfect subtypes. They just want to reuse as much already implemented behavior as possible.

> That syntax is too heavyweight (IMO). I'd be fine with something more compact for the default case of "steal all behavior except what is explicitly overridden", such as: class Related like Base;

Post by catnaroek » Thu, Aug 25, 2016, 5:17 PM UTC

dragonwriter wrote: post #186

catnaroek wrote: post #184

Earlier quoted context omitted.

(0) Do you have a use case for cherry-picking which methods are inherited? If not, it seems like too much complexity for me. (1) Do you think there would still be a use case for “extends”? If not, I'd rather drop it as well.

> Do you have a use case for cherry-picking which methods are inherited? The most obvious is that it makes intent explicit in the case of multiple similarity (I prefer "similarity" to "inheritance" for non-subtyping implementation reuse.) It might in some cases make sense to do this on an interface rather than (or in addition to) single method level; there's probably a lot to work out in the ergonomics of non-subtypi…

Post by naasking » Thu, Aug 25, 2016, 5:39 PM UTC

dragonwriter wrote: post #180

catnaroek wrote: post #175

Earlier quoted context omitted.

Some subclasses can be safely used as subtypes. For example, those that meet the following two conditions: (0) Not directly mutating superclass fields. (Reading them is fine.) (1) Not overriding non-abstract methods of the superclass.

If classes are types, subsclasses should be subtypes -- so the above restrictions should just be applied to subclass relationships. One could also have an non-subclassing mechanism of implementation sharing, that might be declared something like this: class Related does (method1, method2) like Base; or class Related does all except (method3) like Base;