-- https://discourse.haskell.org/t/enforcing-correct-api-usage-via-types/5798

LinearAPI.hs

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QualifiedDo #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE NoImplicitPrelude #-}

-- https://discourse.haskell.org/t/enforcing-correct-api-usage-via-types/5798
module Main where

import Control.Functor.Linear as Linear -- for the linear do-notation using QualifiedDo
import Data.ByteString
import Prelude.Linear (FilePath, Maybe (..), Ur (..), print, show, undefined, ($))
import Prelude.Linear qualified -- for the non-linear IO in the signature of main
import System.IO.Linear

data Mode = ReadMode | WriteMode StoreMode

data StoreMode = StoreAllowed | StoreForbidden

type family FirstKey (mode :: Mode) :: Mode where
  FirstKey ReadMode = ReadMode
  FirstKey (WriteMode _) = WriteMode StoreForbidden

type family NextKey (mode :: Mode) :: Mode where
  NextKey ReadMode = ReadMode
  NextKey (WriteMode _) = WriteMode StoreAllowed

-- In a real libary, the value constructor should be private so that clients
-- can't sidestep the linear discipline
data DB (m :: Mode) = DB

-- We allocate in continuation-passing style
openRead ::
  FilePath ->
  (DB ReadMode %1 -> IO (Ur b)) %1 ->
  IO (Ur b)
openRead = undefined

-- We allocate in continuation-passing style
openWrite ::
  FilePath ->
  (DB (WriteMode StoreAllowed) %1 -> IO (Ur b)) %1 ->
  IO (Ur b)
openWrite = undefined

-- Receives the DB handle but does not return it, so
-- no function can work with it afterwards.
close :: DB m %1 -> IO ()
close = undefined

fetch ::
  ByteString ->
  DB m %1 ->
  IO (DB m, Ur (Maybe ByteString))
fetch = undefined

store ::
  ByteString ->
  ByteString ->
  DB (WriteMode StoreAllowed) %1 ->
  IO (DB (WriteMode StoreAllowed))
store = undefined

-- Changes the StoreMode
firstkey ::
  DB m %1 ->
  IO (DB (FirstKey m), Ur (Maybe ByteString))
firstkey = undefined

-- Changes the StoreMode
nextkey ::
  ByteString ->
  DB m %1 ->
  IO (DB (NextKey m), Ur (Maybe ByteString))
nextkey = undefined

main :: Prelude.Linear.IO () -- this seems to be normal non-linear IO.
main = withLinearIO $ Linear.do
  Ur () <- openRead "/tmp/foo.txt" \db0 -> Linear.do
    (db1, Ur mb) <- fetch "foo" db0
    case mb of
      Nothing -> pure ()
      Just bytes -> fromSystemIO $ print bytes
    close db1
    pure $ Ur ()
  Ur () <- openWrite "/tmp/foo.txt" \db0 -> Linear.do -- compare types of db0 and db1
    (db1, Ur _) <- firstkey db0 -- names, alway more names...
    (db2, Ur _) <- nextkey "foo" db1
    db3 <- store "foo" "bar" db2
    close db3
    pure $ Ur ()
  openRead "/tmp/foo.txt" \foo0 -> 
    openWrite "/tmp/bar.txt" \bar0 -> Linear.do 
        close foo0
        close bar0
        pure $ Ur ()