Parse, don’t type-check

Re:Parse, don’t type-check by tsimionescu on Thursday November 26, 2020 @06:45PM (#25224372)

Of course that type doesn't encode everything there is to know about that function, even assuming purity.

Here are some functions that match that type signature:

    map1 foo x:xs = [foo x]

    mapR foo x:xs = append (mapR foo xs) foo x

    mapI foo x:xs = foo x : mapI foo x:xs

Of course, we can create many more functions that arrange the values in other creative ways, that add more or fewer values etc. If the function isn't pure, we can also imagine many more dimensions of functions that do arbitrarily different things from what you would expect.

If you want complete signatures without dependent types, you need functions which take only single values of different unknown types, like apply: (a -> b) -> a -> b. If you have more than one parameter of the same unknown type, you'll have some ambiguity already.

Non-dependent types can only be used to encode extremely simple properties of a program. They are certainly useful, but they are not in any way the be-all, end-all of static verification.

[ Parent | on HN ]

Re:Parse, don’t type-check by euiq on Thursday November 26, 2020 @09:13PM (#25225048)

> Of course that type doesn't encode everything there is to know about that function, even assuming purity.

Right—we need to require foo id = id.

[ Parent | on HN ]

Re:Parse, don’t type-check by tsimionescu on Sunday November 29, 2020 @08:55AM (#25245105)

That only works because Haskell can't really express it. That is, if you could write Haskell code that checked that equality, that equality wouldn't be enough, because you could write a function `mapStrange foo [x]` that is equal to `map` if `foo = id` and is something else otherwise.

But since you can't compare 2 functions for equality, and you can't compare two arbitrary values for equality, then yes - your informal requirement is enough togethet with the type to force the function to be `map`.

[ Parent | on HN ]