class.fab

class Num a {
  zero :: a
  sub :: a -> a -> a,
  neg :: a -> a = sub zero,
} in
instance (Num Int) {
  zero = 0,
  sub = sub_int,
  neg = neg_int,
} in
instance (Num Float) {
  zero = 0.0,
  sub = sub_float,
} in
neg 0.1

constraints-simplified.fab

// simplified representation of constraints-based type classes
//
// [base_types]
// Int = "*"
// Float = "*"
// [literal_types]
// integer = Int
// number = Float
// [bindings]
// fst = "∀'a 'b 'c. ('a, 'b, 'c) -> 'a"
// snd = "∀'a 'b 'c. ('a, 'b, 'c) -> 'b"
// snd = "∀'a 'b 'c. ('a, 'b, 'c) -> 'c"
// int_of_float = "Float -> Int"
// addInt = "Int -> Int -> Int"
// mulInt = "Int -> Int -> Int"
// negInt = "Int -> Int -> Int"
// addFloat = "Float -> Float -> Float"
// mulFloat = "Float -> Float -> Float"
// negFloat = "Float -> Float -> Float"
//
// this can be easily converted (without type direction) from the source language shown in `constraints.fab`

// from Fig. 7 in P.Wadler, S.Blott 1989 (modified)
type Num = ΛT. constraint numD ((T -> T -> T), (T -> T -> T), (T -> T)) in
let add = fst numD in
let mul = snd numD in
let neg = thd numD in
satisfy (Num Int) = (addInt, mulInt, negInt) in
satisfy (Num Float) = (addFload, mulFloat, negFloat) in
let square = λx. mul x x in
add (square 3) (int_of_float (square 1.2))

==========

// from Fig. 6 in P.Wadler, S.Blott 1989
type Eq = ΛT. eq :: (T -> T -> Bool) in
satisfy (Eq Int) = eqInt in
satisfy (Eq Char) = eqChar in
satisfy (∀'T. ∀'U. Eq 'T => Eq 'U => Eq ('T, 'U)) = λa. λb. eq (fst a) (fst b) && eq (snd a) (snd b) in
// fail satisfy (Eq (Int, Int)) = λa. λb. eqInt (fst a) (fst b) && eqInt (snd a) (snd b) in
eq (1, 'a') (2, 'b')

==========

// multi-parameter example
type Coerce = Λa. Λb. constraint coerce (a -> b) in
type Show = Λa. constraint show (a -> String) in
satisfy (∀'T. Show 'T => Coerce 'T String) = show in
satisfy (Show Int) = string_of_int in
print (coerce 1)

==========

// superclass example
type Eq = ΛT. constraint eq (T -> T -> Bool) in
type Zeroable = ΛT. Eq T => constraint isZero (T -> Bool) in
satisfy (Zeroable Int) = λx. eq x 0 in
// fail satisfy (Zeroable Float) = isZeroFloat in
satisfy (Eq Int) = eqInt in
satisfy (Eq Char) = eqChar in
let iszero1 = λx. isZero x in
// fail iszero1 1.0
iszero1 1

==========

// real-world example (functor, applicative)
// NOTE that type parameter here is not *, but * -> * (HKT)
type Pair = Λa. (a, a) in
type Triple = Λa. (a, a, a) in
type Functor = Λf. constraint fmap (∀'a. ∀'b. ('a -> 'b) -> f 'a -> f 'b) in
type Applicative = Λf. Functor f => constraint pure (∀'a. 'a -> f 'a) in
// satisfy (∀'a. Functor (Either a)) = ...
// ∀'c. constraint fmap (∀'a. ∀'b. ('a -> 'b) -> (Either 'c) 'a -> (Either 'c) 'b)
satisfy (Functor Pair) = λf. λx. (f (fst2 x), f (snd2 x)) in
satisfy (Functor Triple) = λf. λx. (f (fst3 x), f (snd3 x), f (thd3 x)) in
satisfy (Applicative Pair) = λx. (x, x) in
satisfy (Applicative Triple) = λx. (x, x, x) in
let square = λx. x * x in
let squared = λx. fmap square (pure x) in
snd3 (squared 3)

constraints-translation.fab

let add = λnumD_a. fst numD_a in
let mul = λnumD_a. snd numD_a in
let neg = λnumD_a. thd numD_a in
let numD_Int = (addInt, mulInt, negInt) in
let numD_Float = (addFloat, mulFloat, negFloat) in
let square = λnumD_a. λx. mul numD_a x x in
add numD_Int (square numD_Int 3) (int_of_float (square numD_Float 1.2))

==========

let eq_Int = eqInt in
let eq_Char = eqChar in
let eq_TU = λeq_a. λeq_b. λa. λb. eq_a (fst a) (fst b) && eq_b (snd a) (snd b) in
eq_TU eq_Int eq_Char (1, 'a') (2, 'b')

==========

let coerce_Show = λshow_a. show_a in
let show_Int = string_of_int in
print (coerce_Show show_Int 1)

constraints.fab

// Type is Type with kind of Type
// Constraint is Type with kind of Constraint

// Source Language -> Dictionary Conversion -> Overloading Resolution -> Target Language
// Item = (
//   kind [KindExpr] type [Ident] [Params] = [TypeExpr],
//   satisfy [TypeScheme] { [Defs] },
//   typ [TypeScheme] val [Ident] [Params] = [Expr],
// )
// KindExpr = (
//   Type,
//   Constraint,
//   [KindExpr] -> [KindExpr],
// )
// TypeExpr = (
//   [Ident],
//   [TypeExpr] [TypeExpr],
//   [TypeExpr] -> [TypeExpr],
//   constraint { ... },
//   variant { ... },
// )
// TypeScheme = forall [Idents]. [[TypeExprs] =>] [TypeExpr]

kind Type
type Int = #Int#

kind Type
type Char = #Char#

kind Type -> Type
type List a = variant {
  Nil,
  Cons(a, List a),
}

kind Type
type String = List Char

kind Type -> Type -> Constraint
type a ~> b = constraint {
  coerce :: a -> b
}

kind Type -> Constraint
type Show a = constraint {
  show :: a -> String
}

satisfy (forall T. Show T => T ~> String) {
   into = show
}

satisfy (Show Int) {
   show = string_of_int
}

typ String -> ()
val print = #print#

typ a -> (a -> b) -> b
val a |> b = b a

typ ()
val main = 1 |> into |> print

constraints2.fab

type Coerce a b = constraint {
  coerce (a -> b)
} in
type Show a = constraint {
  show (a -> String)
} in
satisfying (forall T. Show T => Coerce T String) {
   into = show
} in
satisfying (Show Int) {
   show = string_of_int
} in
print (into 1)

constraints3.fab

// from Fig. 6 in Wadler, 1988
type Eq T = constraint {
  eq (T -> T -> Bool)
} in
satisfying (Eq Int) {
  eq = eqInt
} in
satisfying (Eq Char) {
  eq = eqChar
} in
satisfying (forall T, U. Eq T, Eq U => Eq (T, U)) {
  eq a b = eq (fst a) (fst b) && eq (snd a) (snd b)
} in
eq (1, 'a') (2, 'b')

constraints4.fab

// from Fig. 7 in Wadler, 1988 (modified)
type Num T = constraint {
  add (T -> T -> T),
  mul (T -> T -> T),
  neg (T -> T),
} in
satisfying (Num Int) {
  add = addInt,
  mul = mulInt,
  neg = negInt,
} in
satisfying (Num Float) {
  add = addFloat,
  mul = mulFloat,
  neg = negFloat,
} in
let square x = mul x x in
add (square 3) (int_of_float (square 1.2))