I wonder if the efficiency in the head . sort example is a property of all sort algorithms or just some of them, and if the latter, if there is a way to capture that property in the type of the sort function.
Definitely only some; trivially, a bozo sort [1] is a useless but correct sort algorithm which does not have this property.
I don’t believe there’s a way to express performance characteristics in Haskell’s typesystem. In an imaginary strict language, one could implement the equivalent to Haskell’s lazy lists as a thunk that returns (next item, next thunk):
type List a :: () -> Maybe (a, List a)
The () is there because this hypothetical is strictly evaluated, and there’s no really obvious vaguely-ML-ish notation to mean a function of no arguments, since that’s… not really a function in the mathematical sense. :)
One would then implement head like this:
head :: List a -> Maybe a
head items =
case items () of
Just (a, _) -> a
Nothing -> Nothing
If one augmented this typesystem with O() annotations on all the function arrows, and imagined a fanciful syntax for it, one could then write:
type List a :: () -> {time O(1), space O(1)} Maybe (a, List a)
head :: List a -> {time O(1), space O(1)} Maybe a
If one wanted to express that different lists may have different complexities, one could move the complexity annotation to a parameter of the List type constructor!
type List a bigO :: () -> {bigO} Maybe (a, List a)
head :: List a bigO -> {bigO} Maybe a
Then head’s complexity matches the complexity of the underlying list.
I’ve been thinking a lot but from a very amateur perspective, on how typesystems can accommodate this sort of thing. Time and space aren’t the only things one might want to make statements about; if there’s a callback, or any other arbitrary side effect, one might well care about how many times it’s invoked. But annotating is the easy part; the hard work is figuring out the typesystem’s judgement rules, proving its soundness, finding a decision procedure for it, … deciding whether it’s okay if typechecking is undecidable… :)
[1] Construct a copy of the input which has the elements in random order. Check whether they are sorted. If not, repeat. Primarily useful as a rhetorical device. :)
Just as a nit, () -> a has a completely well-defined mathematical meaning as a function. The type () is the type with a single inhabitant and thus functions () -> a are pointers into the values of type a—also known as generalized elements.
Yeah. I’m not entirely clear how what I wrote implied otherwise, but I’m certain there are people who benefited from the clarification, and thank you.
I was giving it () as a parameter because if I give it no parameter at all, the syntax would just be “a”, which in a strict language means something different from “something -> a”… of course there aren’t a lot of strict languages that use the -> notation, so really I’m abusing the notation pretty horribly.
Ah, I think I misread your post as saying that “() -> a” is not a well-defined mathematical function not that the concept of a “function of no arguments” wasn’t. Apologies!
I’d like to add that I’m using a hypothetical strict language for these examples, because laziness makes it awkward to describe performance characteristics even informally. (I know someone’s going to object to that…) There’s not only the resources the function uses when it’s first called; there’s the additional resources which may or may not be used when each portion of its result is inspected, at some later point. So I didn’t want to complicate everything by going into that.
I wonder if the efficiency in the
head . sortexample is a property of all sort algorithms or just some of them, and if the latter, if there is a way to capture that property in the type of the sort function.Definitely only some; trivially, a bozo sort [1] is a useless but correct sort algorithm which does not have this property.
I don’t believe there’s a way to express performance characteristics in Haskell’s typesystem. In an imaginary strict language, one could implement the equivalent to Haskell’s lazy lists as a thunk that returns (next item, next thunk):
The () is there because this hypothetical is strictly evaluated, and there’s no really obvious vaguely-ML-ish notation to mean a function of no arguments, since that’s… not really a function in the mathematical sense. :)
One would then implement head like this:
If one augmented this typesystem with O() annotations on all the function arrows, and imagined a fanciful syntax for it, one could then write:
If one wanted to express that different lists may have different complexities, one could move the complexity annotation to a parameter of the List type constructor!
Then head’s complexity matches the complexity of the underlying list.
I’ve been thinking a lot but from a very amateur perspective, on how typesystems can accommodate this sort of thing. Time and space aren’t the only things one might want to make statements about; if there’s a callback, or any other arbitrary side effect, one might well care about how many times it’s invoked. But annotating is the easy part; the hard work is figuring out the typesystem’s judgement rules, proving its soundness, finding a decision procedure for it, … deciding whether it’s okay if typechecking is undecidable… :)
[1] Construct a copy of the input which has the elements in random order. Check whether they are sorted. If not, repeat. Primarily useful as a rhetorical device. :)
Edit: Pre-wrap the code snippets.
Just as a nit,
() -> ahas a completely well-defined mathematical meaning as a function. The type()is the type with a single inhabitant and thus functions() -> aare pointers into the values of typea—also known as generalized elements.Yeah. I’m not entirely clear how what I wrote implied otherwise, but I’m certain there are people who benefited from the clarification, and thank you.
I was giving it () as a parameter because if I give it no parameter at all, the syntax would just be “a”, which in a strict language means something different from “something -> a”… of course there aren’t a lot of strict languages that use the -> notation, so really I’m abusing the notation pretty horribly.
Ah, I think I misread your post as saying that “() -> a” is not a well-defined mathematical function not that the concept of a “function of no arguments” wasn’t. Apologies!
Not a problem!
I’d like to add that I’m using a hypothetical strict language for these examples, because laziness makes it awkward to describe performance characteristics even informally. (I know someone’s going to object to that…) There’s not only the resources the function uses when it’s first called; there’s the additional resources which may or may not be used when each portion of its result is inspected, at some later point. So I didn’t want to complicate everything by going into that.