Bank account interface as a codata type in Polarity (see: https://polarity-lang.github.io)

bank-account.pol

-- UML Class diagram:
--
-- ┌───────────────────────────────────┐
-- │ BankAccount                       |
-- ├───────────────────────────────────┤
-- │ - owner : String                  |
-- │ - balance : Dollars = 0           |
-- ├───────────────────────────────────┤
-- │ + getOwner() : String             |
-- │ + getBalance() : Dollars          |
-- │ + deposit( amount : Dollars )     |
-- │ + withdrawal( amount : Dollars )  |
-- └───────────────────────────────────┘
--
-- Based on https://en.wikipedia.org/wiki/File:BankAccount1.svg

-- Polarity does not have strings, so just use some hard-coded names
data Owner {
    Alice,
    Sally,
}

data Dollars {
    Z,
    S(pred: Dollars)
}

def Dollars.add(other: Dollars): Dollars {
    Z => other,
    S(x) => S(x.add(other))
}

def Dollars.monus(other: Dollars): Dollars {
    Z => Z,
    S(pred) => other.match {
        Z => S(pred),
        S(pred') => pred.monus(pred')
    }
}

data Option(a: Type) {
  None(a: Type): Option(a),
  Some(a: Type, x: a): Option(a)
}

-- | Bank account interface
codata BankAccount {
    -- | The owner of the account
    .getOwner: Owner,
    -- | The current balance in the account
    .getBalance: Dollars,
    -- | Deposit some money into the account
    .deposit(a: BankAccount, amount: Dollars): BankAccount,
    -- | Withdraw some money from the account, returning `None` in the case of an overdraft
    .withdrawal(a: BankAccount, amount: Dollars): Option(BankAccount),
}

-- | Create an account given the owner and the current balance
codef AccountState(owner: Owner, balance: Dollars): BankAccount {
    .getOwner => owner,
    .getBalance => balance,
    .deposit(a, amount) => AccountState(owner, balance.add(amount)),
    .withdrawal(a, amount) => balance.match {
        Z => None(_),
        S(_) => Some(_, AccountState(owner, balance.monus(amount)))
    }
}

-- | Create a new bank account for a given owner
let createAccount(owner: Owner): BankAccount {
    AccountState(owner, 0)
}

It would be neat if I could make WithStateAccountState local to the let binding to encapsulate the state (as in the UML diagram), but I understand that might be difficult with the defunctionalisation/refunctionalisation stuff in Polarity. This is how I sketched it out in psuedocode:

codata BankAccount
  GetOwner : BankAccount -> String
  GetBalance : BankAccount -> Dollars
  Deposit : BankAccount -> Dollars -> BankAccount
  Withdrawal : BankAccount -> Dollars -> BankAccount

createAccount : String -> BankAccount
createAccount owner = account { owner, balance = 0 }
  where
    account : { owner : String, balance : Dollars } -> BankAccount
    (account a).GetOwner          = a.owner
    (account a).GetBalance        = a.balance
    (account a).Deposit amount    = account { a | balance = balance + amount }
    (account a).Withdrawal amount = account { a | balance = balance - amount }

Yes. This would require local recursive (co)definitions. This is not inherently difficult with de-/refunctionalization, as we lift all local (co)matches of a given type to top-level (co)definitions before de-/refunctionalizing that type. The same would have to apply to local recursive (co)definitions. Still, it would be some effort to implement :)

This is related to this issue but depending on how we design it, it might not be sufficient for this use case.