6 ms·

Higher-Order Type-Level Programming in Haskell [pdf]

155 points by justinhj 8y ago

ggm 8y ago
I understood about one concept in 10 here. Not all of the and and but were understood btw. But, that said, it feels like this is saying something useful, and has a formal proof quality which if correct, has a really strong indication of a useful thing: They say up front that noting issues in backwards compatibility this can make a very big difference to the speed of processing inputs. There is "famous person said so, so it must be true" in this because its hard to contradict SPJ. I don't think I'm even in the corridor, let alone the room of people who could question the logic, but I think the rebuttal needs to be said by somebody who could, if there is one. Notationally I struggle to see how well people could "read" the ascii version of this because they depended on formal logic typography to make the ->> symbol. I don't like ::= and := and -> and ->> risks which are inherent in new mappings into a language, and in type systems I find myself desperately searching for the "said voice" internally which speaks the symbols as a cogent language statement. "is" is such a useful word. "maybe" is such a useful word. "x is an Integer" and "x maybe is an Integer" are easy to understand. How would I "say" ->> to be clear its meaning against is and maybe?
- ximeng 8y ago
  -> could be read as type arrow and ->> as unmatchable type arrow?
  - ggm 8y ago
    can you "speak" a sentence either here written or in your head, using those words, which feels like it makes sense?
    - sitkack 8y ago
      I appreciate your meta-level.
    - ximeng 8y ago
      "As an example, the kind of Maybe remains ⋆ → ⋆, but DbType now has kind ⋆ ↠ ⋆" - the kind of Maybe remains star type arrow star, but DbType now has kind star unmatchable type arrow star.
      - ggm 8y ago
        unmatchable type or not yet matched type? dangling type? provisional type? unconfirmed type?
        ximeng 8y ago
        Unmatchable type, following terminology from the paper. This is contrasted with a matchable type which is "injective" and "generative". Basically these unmatchable types are potentially ambiguous under certain operations, so it indicates to the type system limits to the transformations which can be done. So Maybe is * -> * means that if Maybe a is f a, then f is Maybe, and if Maybe a is Maybe b then a is b. If another type t is * ->> *, then the type checker can't make these assumptions.
    - danidiaz 8y ago
      ->> is a function at the type level without extra properties like matchability, so it can be simply read as "to" or "into" -> is used with type constructors like Maybe or Either, and arguments passed to it can still be "read" in the result (for example, a -> Maybe a, or a -> b -> Either a b). I would call it a "slotting" arrow to connote that the argument will be fitted into a hole of a type constructor. So I would read a -> Maybe a as "slotting a into Maybe".
- wwwigham 8y ago
  The readability of the arrow seems unimportant, as it's primary use is, from what I can tell, to express a new kind of constraint which can then be produced by inference and used to typecheck a wider gamut of input code with more succinct type annotations. Generally the inference engine assumes all type constructors are matchable - meaning they're both generative and injective (while type families are neither). However, if you want to work with an arbitrary type with unapplied generics, you can't really consider it injective, since you don't know what kind it is, or weather the `f a ~ f b => a ~ b` injective relationship actually holds (it could be a type family for which it wouldn't hold). Generativity, on the other hand, primarily impacts inference and the ability to break a type apart to perform inferences on its parts (where, if assumed for higher kinds, could cause the inference engine to potentially "skip past" the desired inferences, from what I can tell). What the paper seems to be about is that by adding this novel constraint, you can start to work with partially applied types, since you simply need to acknowledge that these two rules need not always hold (when dealing with type constructors), and that so long as the solver is aware of where these rules do not hold, a well-typed and sound program can still be produced. While _some_ higher-kinded manipulating code needs the explicit ->> syntax to be well-typed, the authors determined that explicitly requiring it (or, likewise, the polymorphic arrow syntax ->^U) would prevent the intent of older code from changing, while the improved inferences allowed just by the new constraint kinds existing allows new flexibility. Also: I don't think there's anything you could write in the double arrow's place that would be "readable" or "just make sense". I think it's difficult to acquire an innane "sense" for what a higher kinded operation actually _is_. By sticking close to familiar syntax, it should hopefully be easier to grasp as a related concept.
mpoteat 8y ago
I wonder if this formalism can be applied to Typescript. I occasionally come across tricky typing problems with higher order functions like "flatten" that this might be helpful for.
- wwwigham 8y ago
  This is just a guess, but since TS is structural and it's inference engine is based on pattern matching instead of constraint solving some of this already applies. Minimally, the generalized type traversal constructors described as a use for higher kinds are already possible.[1] Then again, it was _also_ already similarly possible in Haskell, just _incredibly_ verbose, as it is there. The concepts don't quite transfer 1:1, due to implementation and type system differences (for example, TS doesn't have a solver relying on certain identities holding to generate new inferences or equations), but I think the gist of it (adding what amounts to a "is possibly a higher kind" constraint) could be portable and form the basis of a higher-kinded algebra in TS and allow for a wider array of patterns to be expressed more succinctly. Unfortunately I'm not immediately sure how structural subtyping would work out for something with that kind of constraint, which would need to be solved, too. [1] https://github.com/DefinitelyTyped/DefinitelyTyped/blob/master/types/ramda/tools.d.ts https://github.com/DefinitelyTyped/DefinitelyTyped/blob/mast...
- fro0116 8y ago
  Being somewhat of a functional programming zealot (coming from the Clojure camp, so please excuse me if these are stupid questions, considering my lack of familiarity with typed functional programming in general), this is something that has always bothered me about TypeScript's type system, the poor support for higher order functions. For a prime example of this, take a look at the type definition for the ramda pipe function: https://github.com/DefinitelyTyped/DefinitelyTyped/blob/master/types/ramda/index.d.ts#L1941 https://github.com/DefinitelyTyped/DefinitelyTyped/blob/mast... It's a hard coded list of 10 signature overrides that allows it to support up to 10 piped functions. Obviously the actual ramda pipe function can support an arbitrary number of piped functions at runtime, but the types as written only supports 10. This seems awfully inelegant and inflexible. I assume there is some fundamental deficiency in TypeScript's type system that forces people to specify types this way, otherwise it would have been rewritten by now. Is higher kinded types what's missing to be able to express higher order functions and functional composition in an elegant way? If so, can someone provide an example of what the type signature of a pipe function would look like with higher kinded types? Any ideas if higher kinded types are being considered as additions in future versions of TypeScript, or if that's even feasible at all?
LeanderK 8y ago
I think it's a major step towards more pleasant type-level programming in haskell. I recently worked on a very type-level heavy side-project and the matchability is a real issue. I think this could drastically simplify the whole singletons-library and would also enable proving stuff via induction entirly in the type-level.

155 points by justinhj 8y ago

ggm 8y ago

I understood about one concept in 10 here. Not all of the and and but were understood btw. But, that said, it feels like this is saying something useful, and has a formal proof quality which if correct, has a really strong indication of a useful thing: They say up front that noting issues in backwards compatibility this can make a very big difference to the speed of processing inputs. There is "famous person said so, so it must be true" in this because its hard to contradict SPJ. I don't think I'm even in the corridor, let alone the room of people who could question the logic, but I think the rebuttal needs to be said by somebody who could, if there is one. Notationally I struggle to see how well people could "read" the ascii version of this because they depended on formal logic typography to make the ->> symbol. I don't like ::= and := and -> and ->> risks which are inherent in new mappings into a language, and in type systems I find myself desperately searching for the "said voice" internally which speaks the symbols as a cogent language statement. "is" is such a useful word. "maybe" is such a useful word. "x is an Integer" and "x maybe is an Integer" are easy to understand. How would I "say" ->> to be clear its meaning against is and maybe?

ximeng 8y ago
-> could be read as type arrow and ->> as unmatchable type arrow?
- ggm 8y ago
  can you "speak" a sentence either here written or in your head, using those words, which feels like it makes sense?
  - sitkack 8y ago
    I appreciate your meta-level.
  - ximeng 8y ago
    "As an example, the kind of Maybe remains ⋆ → ⋆, but DbType now has kind ⋆ ↠ ⋆" - the kind of Maybe remains star type arrow star, but DbType now has kind star unmatchable type arrow star.
    - ggm 8y ago
      unmatchable type or not yet matched type? dangling type? provisional type? unconfirmed type?
      - ximeng 8y ago
        Unmatchable type, following terminology from the paper. This is contrasted with a matchable type which is "injective" and "generative". Basically these unmatchable types are potentially ambiguous under certain operations, so it indicates to the type system limits to the transformations which can be done. So Maybe is * -> * means that if Maybe a is f a, then f is Maybe, and if Maybe a is Maybe b then a is b. If another type t is * ->> *, then the type checker can't make these assumptions.
  - danidiaz 8y ago
    ->> is a function at the type level without extra properties like matchability, so it can be simply read as "to" or "into" -> is used with type constructors like Maybe or Either, and arguments passed to it can still be "read" in the result (for example, a -> Maybe a, or a -> b -> Either a b). I would call it a "slotting" arrow to connote that the argument will be fitted into a hole of a type constructor. So I would read a -> Maybe a as "slotting a into Maybe".
wwwigham 8y ago
The readability of the arrow seems unimportant, as it's primary use is, from what I can tell, to express a new kind of constraint which can then be produced by inference and used to typecheck a wider gamut of input code with more succinct type annotations. Generally the inference engine assumes all type constructors are matchable - meaning they're both generative and injective (while type families are neither). However, if you want to work with an arbitrary type with unapplied generics, you can't really consider it injective, since you don't know what kind it is, or weather the `f a ~ f b => a ~ b` injective relationship actually holds (it could be a type family for which it wouldn't hold). Generativity, on the other hand, primarily impacts inference and the ability to break a type apart to perform inferences on its parts (where, if assumed for higher kinds, could cause the inference engine to potentially "skip past" the desired inferences, from what I can tell). What the paper seems to be about is that by adding this novel constraint, you can start to work with partially applied types, since you simply need to acknowledge that these two rules need not always hold (when dealing with type constructors), and that so long as the solver is aware of where these rules do not hold, a well-typed and sound program can still be produced. While _some_ higher-kinded manipulating code needs the explicit ->> syntax to be well-typed, the authors determined that explicitly requiring it (or, likewise, the polymorphic arrow syntax ->^U) would prevent the intent of older code from changing, while the improved inferences allowed just by the new constraint kinds existing allows new flexibility. Also: I don't think there's anything you could write in the double arrow's place that would be "readable" or "just make sense". I think it's difficult to acquire an innane "sense" for what a higher kinded operation actually _is_. By sticking close to familiar syntax, it should hopefully be easier to grasp as a related concept.

mpoteat 8y ago

I wonder if this formalism can be applied to Typescript. I occasionally come across tricky typing problems with higher order functions like "flatten" that this might be helpful for.

wwwigham 8y ago
This is just a guess, but since TS is structural and it's inference engine is based on pattern matching instead of constraint solving some of this already applies. Minimally, the generalized type traversal constructors described as a use for higher kinds are already possible.[1] Then again, it was _also_ already similarly possible in Haskell, just _incredibly_ verbose, as it is there. The concepts don't quite transfer 1:1, due to implementation and type system differences (for example, TS doesn't have a solver relying on certain identities holding to generate new inferences or equations), but I think the gist of it (adding what amounts to a "is possibly a higher kind" constraint) could be portable and form the basis of a higher-kinded algebra in TS and allow for a wider array of patterns to be expressed more succinctly. Unfortunately I'm not immediately sure how structural subtyping would work out for something with that kind of constraint, which would need to be solved, too. [1] https://github.com/DefinitelyTyped/DefinitelyTyped/blob/master/types/ramda/tools.d.ts https://github.com/DefinitelyTyped/DefinitelyTyped/blob/mast...
fro0116 8y ago
Being somewhat of a functional programming zealot (coming from the Clojure camp, so please excuse me if these are stupid questions, considering my lack of familiarity with typed functional programming in general), this is something that has always bothered me about TypeScript's type system, the poor support for higher order functions. For a prime example of this, take a look at the type definition for the ramda pipe function: https://github.com/DefinitelyTyped/DefinitelyTyped/blob/master/types/ramda/index.d.ts#L1941 https://github.com/DefinitelyTyped/DefinitelyTyped/blob/mast... It's a hard coded list of 10 signature overrides that allows it to support up to 10 piped functions. Obviously the actual ramda pipe function can support an arbitrary number of piped functions at runtime, but the types as written only supports 10. This seems awfully inelegant and inflexible. I assume there is some fundamental deficiency in TypeScript's type system that forces people to specify types this way, otherwise it would have been rewritten by now. Is higher kinded types what's missing to be able to express higher order functions and functional composition in an elegant way? If so, can someone provide an example of what the type signature of a pipe function would look like with higher kinded types? Any ideas if higher kinded types are being considered as additions in future versions of TypeScript, or if that's even feasible at all?

LeanderK 8y ago

I think it's a major step towards more pleasant type-level programming in haskell. I recently worked on a very type-level heavy side-project and the matchability is a real issue. I think this could drastically simplify the whole singletons-library and would also enable proving stuff via induction entirly in the type-level.