Implementing strlen safely

[gmhwxi]

When encountering a programming language, I often ask the question:
How strlen, which computes the length of a given C-style string, should be implemented
in this language?

Here is a way to implement strlen safely in ATS:

fun
strlen{n:nat}
(
  str: string(n)
) : int(n) = let
//
fun loop{i,j:nat}
  (str: string(i), j: int(j)): int(i+j) =
  if isneqz (str) then loop (str.tail, succ(j)) else j
//
in
  loop (str, 0)
end // end of [strlen]

If a language does not allow you to implement strlen, then the language is probably not well-suited
 for low-level programming.

However, most languages suited for low-level programming usually do not allow you to implement strlen
safely.

[Artyom Shalkhakov]

Hello Hongwei,

понедельник, 17 февраля 2014 г., 4:33:11 UTC+6 пользователь gmhwxi написал:

When encountering a programming language, I often ask the question:
How strlen, which computes the length of a given C-style string, should be implemented
in this language?

Here is a way to implement strlen safely in ATS:

fun
strlen{n:nat}
(
  str: string(n)
) : int(n) = let
//
fun loop{i,j:nat}
  (str: string(i), j: int(j)): int(i+j) =
  if isneqz (str) then loop (str.tail, succ(j)) else j
//
in
  loop (str, 0)
end // end of [strlen]

I'm wondering what does this [str.tail] syntax stand for? In ATS1 there was a function that basically returned an incremented pointer to the string (i.e., a tail of the string). Does the syntax expand to a regular function call?
 

[gmhwxi]

Hi Artyom,

str.tail expands to string_tail(str):

fun string_tail {n:pos} (string(n)): string(n-1)
overload .tail with string_tail

This is called dot notation overloading in ATS.