Coding 2024-11-25

Tags:
By Max Woerner Chase

All right, I'm looking over the COCHIS paper, and I want to try just translating the examples to my sketch syntax for Impliciula and see where things go wrong.

The first sample to look at deals with ordering, and depends on the less-than-or-equal-to function. We might translate this arrangement something like:

let module type Ord be signature
  type t
  {<=} (t, t -> bool)

let {<=}
  with implicit module O(Ord where t is 'a)
be ('a, 'a -> bool)
  O.{<=}


let implicit module IntOrd be
  let type t be int
  let {<=} be (int, int -> bool) Int.{<=}

let implicit module CharOrd be
  let type t be char
  let {<=} be (char, char -> bool) Char.{<=}

let implicit module PairOrd
  with implicit module O1(Ord) and implicit module O2(Ord)
be
  let type t be O1.t * O2.t
  iff v0 (t) <= v1 (t) then
    v0[0] <= v1[0] and {not {v1[0] <= v0[0]} or {v0[1] <= v1[1]}}

let sorted: l (list-of: 'a)
  with implicit module O(Ord where t is 'a)
be (list-of: 'a)
  ...

Among other things, I haven't really nailed down the tuple syntax. Regardless...

I'd say a key difference between that sample and the bits of the COCHIS paper that I'm adapting is that I'm using modules, so they're not explicitly parameterized by the type, and instead have to match it with where-clauses and attributes. This might or might not totally break COCHIS, we'll see.

Reading ahead, we see that, at least in Haskell, a blanket implementation of a typeclass allows leaving the typeclass requirement off of a function definition. (I think. I'm not totally sure I'm reading this right.) That sounds like something I don't want to do in Impliciula.

Anyway, I got to the Scala section and my eyes glazed over a little. I'm going to assume that's a "me" problem, and I should start winding down a little early.

Good night.