Skip to content

Instantly share code, notes, and snippets.

@Savelenko
Savelenko / Pete.fs
Created October 14, 2022 16:40
Pete wrapper and bind
type Pete<'T> (wrapped : 'T) =
member this.Bind (binder : 'T -> Pete<'U>) : Pete<'U> =
binder wrapped
@Savelenko
Savelenko / VehicleMaintenance.fs
Created October 11, 2022 09:22
Modeling vehicle maintenance with GADTs in F#
module VehicleMaintenance
open TypeEquality // See my other gists for this module
(*
A vehicle shop can perform certain maintenance procedures on cars and bicycles. Every maintenance procedure has a price.
For bicycles prices are fixed. For cars the price may depend on engine capacity.
*)
// Vehicles and prices
@Savelenko
Savelenko / Program.fs
Last active November 14, 2022 12:56
A modeling exercise in two acts with banning or verifying users in F# and the Onion architecture
(*
An exercise in modeling. Users can be verified or banned. A user can be banned only if their username is "offensive".
We assume the Onion architecture. Modules `User` and `Verification` belong to the model. Module `UserVerification`
belongs to the application layer. Data access layer is omitted completely; it should be fairly trivial.
Note that the verified/banned aspect of a user is modeled "externally" to the notion of user itself. In particular,
there are no "aggregates" below which combine all aspects of a user.
*)
@Savelenko
Savelenko / Explanation.fs
Last active September 6, 2022 11:09
Ghosts of departed proofs using F#
module Explanation
(*
So what is going on in module `ValidatedSum`? This is a more detailed explanation and a piece of guidance. The goal of
all of this is being able to define libraries with "safe" APIs. To be more precise, "safe" means that functions with
interesting preconditions can only be used (applied) such that the precondition is guaranteed to hold; it is impossible
to apply a function on inputs for which the precondition does not hold.
A well-known example is `List.head`. The precondition of applying this function to list `l` is that `l` is non-empty. If
@Savelenko
Savelenko / Money.purs
Created July 15, 2022 12:57
Representing money in PureScript using phantom types and symbols
newtype Money currency = Money Number -- Constructor is not exported
sumMoney :: forall currency. Money currency -> Money currency -> Money currency
sumMoney (Money a) (Money b) = Money (a `add` b)
infixl 6 sumMoney as +
multiplyMoney :: forall currency. Number -> Money currency -> Money currency
multiplyMoney multiplier (Money a) = Money (multiplier `mul` a)
@Savelenko
Savelenko / Encodable.fs
Created June 29, 2022 13:37
Data format selection with static abstract member-based encoder
type IEncodable<'t> =
static abstract Encode : 't -> byte[]
/// Selects Base64 encoding for `a`.
type Base64<'a when 'a :> IEncodable<'a>> = Base64 of 'a with
interface IEncodable<Base64<'a>> with
member this.Encode (Base64 a) =
let toBase64 = failwith "..."
toBase64 ('a.Encode a)
@Savelenko
Savelenko / Validation2.fs
Created June 14, 2022 08:29
Applicative validation with abstract static interface members
(*
The original applicative validation type is defined like this in FsToolkit.ErrorHandling:
*)
/// Validation<'a, 'err> is defined as Result<'a, 'err list> meaning you can use many of the functions found in the
/// Result module.
type Validation<'ok, 'error> = Result<'ok, List<'error>>
(*
We can abstract the `List` away by requiring any structure which supports concatenation, of which the list's (@) is an
@Savelenko
Savelenko / Facility.fs
Created May 26, 2022 09:35
Error builder
module Facility
/// A facility which admits visitors (or does it?).
type Facility =
| BlackMesa
| DeathStar
| TeaHouse
(*
@Savelenko
Savelenko / Giraffe.purs
Created September 21, 2021 10:02
Giraffe computation expression (PureScript prototype)
module Giraffe where
import Prelude
import Control.Monad.Cont (Cont, callCC, cont, lift, runCont)
import Control.Monad.Reader (ReaderT, ask, runReaderT)
import Data.Maybe (Maybe(..))
data HttpContext = HttpContext
type HttpFuncResult = Maybe HttpContext -- Task<Option<..>> actually, but ignore Task for simplicity here
@Savelenko
Savelenko / Json.fs
Last active June 24, 2021 11:06
Church-encoded JSON in F#
/// Church-encoded JSON values.
type Json =
abstract Value<'r> :
(string -> 'r)
-> (bool -> 'r)
-> (decimal -> 'r)
-> (Map<string, Json> -> 'r)
-> (List<Json> -> 'r)
-> 'r