I think understanding the expressivity of the DOT approach vis-a-vis the more conventional 1ML approach should be interesting. 1ML is based on F-omega, which h

I think understanding the expressivity of the DOT approach vis-a-vis the more conventional 1ML approach should be interesting. 1ML is based on F-omega, which has higher kinds but not dependent sums or products, while D_{<:} has path-dependent products but no apparent higher kinds, if I understand the paper correctly.