kongware / scriptum

Functional Programming Unorthodoxly Adjusted to Client-/Server-side Javascript
MIT License
383 stars 21 forks source link

Allow existential types in the context of data constructors #345

Closed ivenmarquardt closed 3 years ago

ivenmarquardt commented 3 years ago

This will allow the following type:

const Coyoneda = type1("^b. (b => a) => f<b> => Coyoneda<f, a>").

Prerequisit for this feature is that it only affects the type1 newtype constructor. Since there is no pattern matching for newtypes in scriptum there shouldn't be a problem. For more information read existentials in GHC.

Record types are another context where existential types make a lot of sense but scriptum won't support existential record types for the time being.

ivenmarquardt commented 3 years ago

Unfortunately, existentials have an impact on unification. I not gonna open Pandora's Box again. With scriptum we'll have to resort to higher-rank types to overcome this shortcomming:

const Coyoneda = type1("(^b, r. ((b => a) => f<b> => r) => r) => Coyoneda<f, a>")

ivenmarquardt commented 3 years ago

Existentials are incredible useful. For instance, they allow the composition of a non-deterministic list of functions. I reckon there is no other way than to open Pandora's Box and extend the unification algorithm. This will take at least a week. Here we go.

ivenmarquardt commented 3 years ago

Subsumed under #346