function effects

[Dambaev Alexander]

ATS2 supports function effects. ie:

```

extern fn

  print

  ( String

  ):<1>

  void

```

IIRC, there was an opinion that ATS3 should not support such feature.

Recently, I have found yet another usecase where such effects are useful: dependency-injection.

In a haskell-world it is known as Handler-pattern and it comes down to:

```

import qualified System.IO as IO

data IOT m = IOT

  { putStrLn :: Monad m => Text-> m () -- m - is an abstract monad, which will be resolved later at link-time

  }

data Call request response = Call (Maybe request) (Maybe response)

data CoreRequest =

  Ping (Call Int Int)

handle_request

  => IOT m

  -> CoreRequest

  -> m ()

handle_request (Ping (Just arg) _ ) = Ping (Just arg) (Just arg)

core

  :: Monad m

  => IOT m

  -> CoreRequest

  -> m CoreRequest

core iot request = do

  iot.putStrLn "hello world" -- this is not a type error, as we are inside monad m and iot has type `IOT m` => m = m, so type checks

  -- IO.putStrLn "hello world" -- this won't compile, as we are inside `m` monad and m != IO, so type error

  handle_request iot request

production_iot :: IO (IOT IO)

production_iot = return $! IOT

  { putStrLn = IO.putStrLn -- here we can use IO.putStrLn :: IO () as type says that we produce concrete type `IOT IO` and thus m = IO

  }

main :: IO ()

main = do

  iot <- production_iot -- here iot is of type (IOT IO) and thus, abstract monad `m` from type definition will be resolved to IO

  request <- read <$> readLine

  response <- core iot request -- here we pass the iot into core, compiler sees, that: 1. we are inside IO monad (main :: IO ()); 2. iot is of type `IOT IO` and thus `core iot` will be resolved into `IO ()`, ie, only at this step we can assume, that members of the IOT datatype is using `IO` monad

  print (show request)

```

this allow us to assume, that inside `core` we can have a pure core of the program, which is only able to use monad `m` or pure functions => ie, `core` is pure.

Then, we can provide mocked version of `IOT`, which logs usage of it's members like:

```

data IOTRequest 

  = PutStrLn 

    { args: String

    }

data AppRequest

  = IOTRequest IOTRequest

mock_iot :: IO (TVar [AppRequest], IOT IO)

mock_iot = do

  logV:: (TVar [AppRequest]) <- newTVarIO

  return $! IOT

    { putStrLn = \str -> do

        STM.atomically $ do

          TVar.modifyTVar logV (++[ IOTRequest (PutStrLn str)])

    }

```

then, we can use such mocked iot during fuzzy testing like. For example, we can test if any request calls `PutStrLn "hello world"`:

```

prop_always_says_hello_first :: Property

prop_always_says_hello_first = monadicIO $ do

  (logV, iot) <- run mock_iot

  request <- arbitrary -- randomly chosen request

  response <- run (core iot request)

  assert ( requestShouldMatchResponse request response)

  log <- run $! STM.atomically $ TVar.readTVar logV

  assert ( List.head log == IOTRequest (PutStrLn "hello world"))

```

and it turned out, that it is possible to achieve something similar with ATS2:

```

datatype IOT = 

  @{ putStrLn = (String) -<cloref> void -- here is the key concept: we define IOT member as pure function

      }

typedef Call (request: t@ype, response: t@ype) = Call of @( Option(request), Option(response))

datatype AppRequest =

  | Ping of Call(int, int)

fn

  handle_ request

  ( iot: IOT

  , request: AppRequest

  ):<>

  AppRequest =

  ( case request of

  | Ping(Some(arg), _ ) => Ping(Some(arg), Some(arg))

  )

fn

  core

  ( iot: IOT

  , request: AppRequest

  ):<> -- here the main idea is to keep core as pure, which will not allow to use impure functons inside
AppRequest = 

  let

    val () = iot.putStrLn( "hello world")

  in

    handle_request( iot, request)

  end

fn

  production_iot

  (

  ):

  IOT = 

  @{ putStrLn = lam str=<cloref> ($UN.cast{(String)-<> void} println) (str) -- here we use cast to wrap println into a pure function

      }

implement main0() = {

   val iot = production_iot()

   val request:AppRequest = readln() 

   val response = core( iot, request)

   val () = println!( show<AppRequest>(response)) -- assume show implemented

}

```

so this is quite similar to haskell's version and by relying on the effect system. Haskell has `Safe Haskell` (compiler pragmas: Safe, Unsafe, Trustworthy ). This feature adds constraints to module system: Safe module can only import other Safe modules and Trustworthy modules. Trustworthy modules can import: Safe, Trustworthy and Unsafe modules. By default, all modules are Unsafe. And unsafe functions (like 'unsafe.sats`) are unsafe and can't be imported by Safe modules. And thus, compiler can guarantee that pure core, which is in Safe module won't use unsafe code unless it is wrapped into Trustworthy modules. And then, if something "bad" happened you know that you need to check Trustworthy modules as core is pure and Safe

I think ATS can benefit from the similar safe/trustworthy/unsafe module system especially with the effect system

So: 1. what is the status of the effects system in ATS3? 2. can I hope that similar Safe/trustworthy/unsafe module system will be adopted by ATS as well? :)

[Hongwei Xi]

In ATS, effect tracking is separate from type-checking.

To me, merging effect tracking with type-checking is a problematic design.

I prefer an "open" design for effect tracking: Instead of relying on the type-checker

to track effects, a separate control-flow analyzer can be implemented for tracking

some special effects. Basically, I hope that the community can implement all sorts

of plug-ins for tracking various effects.

Also, after separating effect tracking for type-checking, one can choose to do the

former at a later stage in compilation.

>> So: 1. what is the status of the effects system in ATS3? 2. can I hope that similar Safe/trustworthy/unsafe module system will be adopted by ATS as well? :)

I am pretty sure that the kind of example you mentioned will be supported. And we will go

beyond, For instance, tracking lock usage; supporting certain functionalities of p_trace at

compile-time; etc.

Cheers,

--Hongwei

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KwOuEEmziui7B1Mw5kjionmWy6tje574HzgQszWrdRSgQ%40mail.gmail.com.