Discussion: Comment style for documentation generation

[EliasC]

This issue is for discussing how we should write comments that can be parsed by a documentation generator (à la Doxygen). It can be seen as a continuation of the discussion started in #175.

The typical way of doing this is to have a special sequence at the start of a comment to signify that this comment can be parsed by a documentation generator. For example, Doxygen (for C and C++) and Javadoc uses double asterisks:

/**
 * This is a Doxygen/Javadoc comment
 * (starting each line with an asterisk is optional)
 */

Doxygen also supports other styles:

/// This is a Doxygen comment using two or more
/// single line comments with triple slashes

/*!
This is a Doxygen comment starting with "*!"
*/

//! This is a Doxygen comment using two or more
//! single line comments starting with "//!"

Haddock (for Haskell) uses a similar style, with | as the special symbol:

-- | This is a Haddock comment, but only the starting line
-- needs to start with a pipe

{- |
  This is a Haddock block comment 
-}

Additionally, Haddock supports documentation both before and after declarations, using ^ to signify that a comment is about the thing above it:

-- | An interesting function
foo :: Int -> Int
foo x = ...

foo :: Int -> Int
-- ^ An interesting function
foo x = ...

In my opinion there are at least two things that warrant discussion:

1. What should our documentation strings look like? Since Updated the syntax for multiline comments. #175, the comment style for Miking is -- for line comments and /- ... -/ for block comments, and it seems reasonable for us to use a similar style to the examples above, i.e., starting a comment with a special character that signifies that we're dealing with documentation. At a meeting there was a hypothesis that line comments should be enough for documentation comments.
2. What kind of information do we want to encode in our documentation. I think this is the more interesting question, and it should be what drives the answer to question 1. The obvious thing that comes to mind is documentation for functions and datatypes, but with a slightly wider focus we might also want to write documentation for utests, language fragments, or even entire files.

As a starting point for the discussion, let's try to write the documentation for the map function. I will be using Haskell's syntax for now, but this should not be seen as endorsement:

-- | `map f s` applies the function `f` to each element of the sequence `s`
let map = lam f . lam seq .
  ...

Some observations:

• It is nice to have some way of formatting code, e.g. using `.
• The names of the parameters need not match the names in the documentation. This makes sense, as there may not always be any parameters:

  -- | `incrAll l` adds one to each element in `l`
  let incrAll = map (addi 1)

• There are currently no types, and with the current syntax the types would be scattered over the code:

  let map = Lam a. Lam b. lam f : a -> b. lam seq : Seq a.
    ... : Seq b

  An alternative way to write it might be

  let map : all a . all b . (a -> b) -> Seq a -> Seq b =
    lam f . lam seq .
      ...

  Regardless of syntax, it would be nice to be able to tie the documentation to a type, so that the type cannot be updated without also updating the documentation. Haskell does this by interspersing comments into the type signature. For us, it might look something like this:

  let map :
    -- | Map a function over a sequence
    all a . all b .
      (a -> b) -> -- | The function to be mapped
      Seq a ->    -- | The sequence to map over
      Seq b =
        lam f. lam seq.
          ...

  (NB: Haddock uses -- ^ for documenting the parameters, since they come before the comment)
  While this could probably generate nice looking documentation, it's starting to make reading the source code less nice.

I think this is enough to get the discussion going!

[johnwikman]

Less of a comment and more an additional example, here is a riff on Doxygen except that it is slightly more verbose, pedantic, and based on indentation:

--*
-- Brief: Checks equality between two Either values.
--
-- Lambdas:
--   eql: Function that checks left equality
--   eqr: Function that checks right equality
--   e1:  Either value to be compared
--   e2:  The other Either value to be compared
--
-- Return: Whether e1 and e2 are equal based on the provided equaliy
--         functions.
--*
let eitherEq: (a -> c -> Bool) -> (b -> d -> Bool) -> Either a b -> Either c d -> Bool =
  lam eql. lam eqr. lam e1. lam e2.
  match (e1,e2) with (Left c1, Left c2) then
    eql c1 c2
  else match (e1,e2) with (Right c1, Right c2) then
    eqr c1 c2
  else
    false


/- How it generally would work: -/
--*
-- <key>: Contents associated with this key follows straight after the colon sign
--  or on the following rows as long as the content is indented at least one space
--    more than the key. There can be
--
--   line breaks between content as long as the indentation rule is preserved.
--   Certain keys such as "Lambdas" can have subkeys, where the content itself
--   are key-content associations:
--
-- Lambdas:
--   <subkey>: Content follows same indentation rule
--     for subkeys as for "top-level" keys.
--   <subkey>: More content
--*

[johnwikman]

Regardless of syntax, it would be nice to be able to tie the documentation to a type, so that the type cannot be updated without also updating the documentation. Haskell does this by interspersing comments into the type signature. For us, it might look something like this:

let map :
  -- | Map a function over a sequence
  all a . all b .
    (a -> b) -> -- | The function to be mapped
    Seq a ->    -- | The sequence to map over
    Seq b =
      lam f. lam seq.
        ...

I also like the concept of tying documentation closer to the code, but only if it doesn't impair code readability. When chasing a bug, I prefer the code to be structured such that it is easy to skim through and find the expression that doesn't belong. How the example above intersperses documentation with the types makes it more difficult for me to read the code. Though maybe this is something that one could get used to.