3 ms·

Something I looked for on this very intriguing site was a reconciliation in my mind between dependent types and higher kinded types. This has been a nagging qu

Something I looked for on this very intriguing site was a reconciliation in my mind between dependent types and higher kinded types. This has been a nagging question since the announcement of Scala moving to the DOT calculus[1]. While this page[2] helped a bit, doing more research unveiled an example put out by Runar here[3]. Has anyone else considered a reasonable method for addressing what higher-kinded types provide currently in a DOT calculus, especially as it pertains to "matching" the type parameters in a higher-kinded type? 1 - http://lampwww.epfl.ch/~amin/dot/fool.pdf http://lampwww.epfl.ch/~amin/dot/fool.pdf 2 - http://ncatlab.org/nlab/show/dependent+type+theory http://ncatlab.org/nlab/show/dependent+type+theory 3 - https://gist.github.com/runarorama/33986541f0f1ddf4a3c7 https://gist.github.com/runarorama/33986541f0f1ddf4a3c7

deleted 11y ago
[deleted]
mafribe 11y ago
reconciliation in my mind between dependent types and higher kinded types. They are orthogonal concepts. This is made very clear in Barendregt's λ-cube [1]. Orthogonal here means that a typing system might be higher-kinded without allowing type-dependency, or it might allow type-dependency without having higher-kinds. An example of the latter is LF, the Logical Framework of Harper et al. Haskell, or at least some forms of Haskell are an example of the former. Higher-kinded types simply allow functions and function application at the type level which can take functions as arguments and can return functions. For example (lambda x.x => bool) and (lambda xy. x => y) are functions at the type level. An example of a dependent type is List(2+4)[bool], of lists of length 6 carrying booleans. Here (2+4) is a program. This parameterisation happens without having type-functions. [1] https://en.wikipedia.org/wiki/Lambda_cube https://en.wikipedia.org/wiki/Lambda_cube

deleted 11y ago

[deleted]

mafribe 11y ago

reconciliation in my mind between dependent types and higher kinded types. They are orthogonal concepts. This is made very clear in Barendregt's λ-cube [1]. Orthogonal here means that a typing system might be higher-kinded without allowing type-dependency, or it might allow type-dependency without having higher-kinds. An example of the latter is LF, the Logical Framework of Harper et al. Haskell, or at least some forms of Haskell are an example of the former. Higher-kinded types simply allow functions and function application at the type level which can take functions as arguments and can return functions. For example (lambda x.x => bool) and (lambda xy. x => y) are functions at the type level. An example of a dependent type is List(2+4)[bool], of lists of length 6 carrying booleans. Here (2+4) is a program. This parameterisation happens without having type-functions. [1] https://en.wikipedia.org/wiki/Lambda_cube https://en.wikipedia.org/wiki/Lambda_cube