Re: [ghc-steering-committee] [ghc-proposals/ghc-proposals] Support ergonomic dependent types (#378)

(Writing to the committee rather than polluting the DT proposal thread.)
We have a bullet "Does not create a language fork" in the review criteriahttps://nam06.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fghc-proposals%2Fghc-proposals%23review-criteria&data=04%7C01%7Csimonpj%40microsoft.com%7C2d39084e129047d031f508d8e3044dca%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637508954935323802%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C1000&sdata=F0fX%2BB%2BjH7xfJWoiYxNOfJRFvo6vix6HhwID5%2FXt1EU%3D&reserved=0. I treat it like the other criteria, a fork-like proposal is a red flag, but not an automatic reject.
This relates back to our earlier conversation about proposal properties. Eric suggested:
* Backward compatibility. Does an extension *expand* the language or *change* it? In other words, does an extension strictly accept more programs than before, or can it change the meaning of existing programs, or even reject previously valid programs?
* Plausible default. Do we expect the extension to eventually be on-by-default (in GHCxxxx) and effectively disappear, or will it continue to be opt-in? -XStrict or -XRebindableSyntax are examples of an extension that we want, but that are not plausible defaults.
* Localised. Is an extension *contained* within a module or is it *infectious*? Does my choice of extensions when writing a module affect which extensions downstream clients must enable? (I would say most extensions are contained, e.g. you can apply a type family without enabling TypeFamilies or match on a pattern synonym without enabling PatternSynonyms. However, you cannot call a function that takes an implicit parameter without enabling ImplicitParams.)
Reading our "fork-like" criterion, it seems to be saying "it's fork-like if it is not a plausible default (in the above sense), and fork-like is bad". But as -XStrict and -XRebindableSyntax show, not being a plausible default isn't necessarily bad.
Do we want to revise our language in the criteria?
Simon
From: Eric Seidel
participants (1)
-
Simon Peyton Jones