Kind: A Modern Proof Language

Re:Kind: A Modern Proof Language by thewakalix on Wednesday August 11, 2021 @04:04PM (#28147022)

> For example, working with Maybe is often frustrating in functional languages. In Kind, we have a default operator: [<>]

While (<>) in Haskell already means a monoidal operator, something similar is frequently defined, such as:

    (:?) :: Maybe a -> a -> a
    (:?) = flip Data.Maybe.fromMaybe

(Making an alternative or supplemental Prelude out of functions like this is a common step in the evolution of a Haskell programmer, like writing a monad tutorial.)

> An "abort" operator, that flattens your code:

That particular function can be written even more concisely in Haskell:

    sumFirst3 :: [Natural] -> Natural
    sumFirst3 list
      | (x : y : z : _) <- list = x + y + z
      | otherwise = 0

And in other cases, the Either monad provides the same logic:

    sumFirst3' :: [Natural] -> Natural
    sumFirst3' list = fromEither do
      x <- list !!? 0 `abort` 0
      y <- list !!? 1 `abort` 0
      z <- list !!? 2 `abort` 0
      return $ x + y + z

    abort :: Maybe a -> e -> Either e a
    abort (Just a) _ = Right a
    abort Nothing e = Left e

(fromEither and (!!?) are utility functions like (:?). For that matter, abort is just a shorter name for maybeToRight.)

> And, of course, Maybe monad:

As it happens, you can write Haskell with braces if you really want to! [0]

[0] https://en.wikipedia.org/wiki/Haskell_features#Layout

[ Parent | on HN ]

Re:Kind: A Modern Proof Language by LangMakers on Wednesday August 11, 2021 @04:13PM (#28147130)

You're forced to be in the Either monad to use your `abort` though, which kinda beats the point (you could just use the Maybe monad...). It is refreshing to be able to just throw an abort literally anywhere in your code, and get rid of a `Maybe` without changing the structure of your code, resting assured that the `none` case is dealt with properly.

[ Parent | on HN ]

Re:Kind: A Modern Proof Language by lmm on Thursday August 12, 2021 @12:08AM (#28151783)

Isn't that the whole point of MTL-style typeclasses? You use e.g. throwError and can be confident that it'll be plumbed appropriately for whichever context you're currently in. Maybe shouldn't be a special case.

[ Parent | on HN ]