Skip to content

Instantly share code, notes, and snippets.

@Savelenko
Last active March 17, 2023 09:13
Show Gist options
  • Save Savelenko/f9e4f7dd2d9a8256156f138c6855bfd6 to your computer and use it in GitHub Desktop.
Save Savelenko/f9e4f7dd2d9a8256156f138c6855bfd6 to your computer and use it in GitHub Desktop.
Meetings and locations model using simulated GADTs in F#
module EmployeeLocation
open TypeEquality
type Name = string
/// Some employees are engineers.
type Engineer = Engineer of Name
/// Some employees are factory workers.
type FactoryWorker = FactoryWorker of Name
/// The company has offices. Each office room has a number.
type OfficeRoom = OfficeRoom of int
/// The company has a factory. A factory has different work areas at different floors.
type FactoryFloor =
| Assembly
| Electronics
| QualityControl
/// A description of a (your) meeting with a single employee. Based on whom you want to talk to, the type of location
/// for the meeting is fixed. However the _actual_ location is not included in values of this type.
type MeetingRequest<'location> =
| TalkToEngineer of Engineer * TEq<OfficeRoom,'location>
| TaltToFactoryWorker of FactoryWorker * TEq<FactoryFloor,'location>
/// A helper for creating a meeting request with an engineer.
let meetingWithEngineer engineer = TalkToEngineer (engineer, TypeEquality.refl)
/// Similarly, a helper for creating a meeting request with a factory worker.
let meetingWithFactoryWorker factoryWorker = TaltToFactoryWorker (factoryWorker, TypeEquality.refl)
(* The most interesting function: given a meeting request, determine the location of the meeting. Each location is
consistent with the meeting request, namely whom the meeting is with. The function looks completely polymorphic in its
return type, which would mean that it can return nonsense location types like `bool`, but this is not the case and only
proper location types are possible. *)
/// Determine the location for a requested meeting.
let meetingLocation (meeting : MeetingRequest<'location>) : 'location =
match meeting with
| TalkToEngineer (Engineer name, forEngineer) ->
// We could go to the database here, but here is a simple simulation
let room = if name = "Peter" then OfficeRoom 1 else OfficeRoom 2
room |> TypeEquality.coerce forEngineer
| TaltToFactoryWorker (FactoryWorker _, forFactoryWorker) ->
// All factory meetings should happen at the electronics floor because they have nice chairs
let allFactoryMeetingsAtElectronics = Electronics
allFactoryMeetingsAtElectronics |> TypeEquality.coerce forFactoryWorker
let example1 : OfficeRoom = meetingLocation (meetingWithEngineer (Engineer "Link"))
let example2 : FactoryFloor = meetingLocation (meetingWithFactoryWorker (FactoryWorker "Zelda"))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment