4 ms·
Not really, Rossberg’s 1ML / F-ing modules provides a way to elaborate such type to plain System F types, i.e. existentials, but not dependent types. The type
by tomp 6y ago
Not really, Rossberg’s 1ML / F-ing modules provides a way to elaborate such type to plain System F types, i.e. existentials, but not dependent types.
The type of such monoid would be:
exists[T] . (M : [= T], f : T -> T, e : T)
- lmm 6y agoSure, but that's distinctly not the way you'd write or think about that definition in everyday mathematics. It encodes the definition but it doesn't really express it.
- GregarianChild 6y agoI think you need HKTs, in other words System F-omega, to carry out Rossberg's idea.
- tomp 6y agoOnly for applicative functors (i.e. OCaml’s version, where Set[int].t == Set[int].t), which 1ML models as pure functions.