4 ms·
What you are looking for is called "dependent types" and is the same mechanism that you have to have to prevent the function you seem to insist is so obviously
by saurik 3y ago
What you are looking for is called "dependent types" and is the same mechanism that you have to have to prevent the function you seem to insist is so obviously to you the right way to do it from also being wrong by returning an offset past the end of the string. Being able to express such things as "this function returns an integer which is between 0 and the length of the string passed as the second argument" and "this function returns a sequence which is related in some way to the sequence passed as an argument" is a reasonable thing to want, but almost no programming languages provide the mechanism to do it; that said, the languages which do--such as Idris or Coq--look a LOT closer to Haskell than Python.
- mrkeen 3y ago> returning an offset past the end of the string I feel if you're dealing with offsets into strings, it's probably easier to stop doing that rather than try to get the type checker to prove it 'correct'. I tried a linear types implementation: newtype Parser a = P (String ⊸ (String, Maybe a)) parseChar :: Char -> Parser Char parseChar c = P $ \s -> case s of [] -> ([], Nothing) (x:xs) -> if x == c then (xs, Just c) else (xs, Nothing) This guarantees that the 's' is used exactly once instead of dropped on the floor. It's not great because I wanted to drop it on the floor. Here's it not compiling when I use the wrong string: ... then ("some string", Just c) ... • Couldn't match type ‘'Many’ with ‘'One’ arising from multiplicity of ‘s’ • In the second argument of ‘($)’, namely ‘\ s -> case s of