How would you define map?

[danvk]

Hello! I enjoyed the paper and playing around with the demo. I tried to define a map function:

let rec map = fun fn -> fun lst -> if lst then { head=fn(lst.head); tail=map fn lst.tail } else false

let lst = {head=1; tail=false}
let addLst = map succ lst

and get this:

val map: ('a -> 'b) -> (bool ∧ {head: 'a, tail: 'c}) as 'c -> (bool ∨ {head: 'b, tail: 'd}) as 'd
val lst: {head: int, tail: bool}
Type error in addLst: cannot constrain bool <: {tail: 'a ∨ bool}

So that's not quite right. How would you define this?

[LPTK]

Hi Dan!

To do what you want nicely, we'd need algebraic data types or the like, which are not implemented here (but are easy to add). Unlike JavaScript there is no "falsiness" and you can't just use a list as the condition in an if-then-else!

We need something like an option type to express the fact that we may have an empty list. One way to emulate an Option T is to use a fold function instead, of type (T -> a) -> ({} -> a) -> a – it takes a function to apply if the option is defined, and an function to apply if the option is empty. Here is what I mean more concretely:

let some = fun x -> fun ifSome -> fun ifNone -> ifSome x
let none = fun ifSome -> fun ifNone -> ifNone{}

let rec map = fun fn -> fun lst ->
  lst (fun cons -> some {head=fn cons.head; tail=map fn cons.tail}) (fun nil -> none)

let lst = some {head=1; tail=none}
let addLst = map succ lst

This works, though the types are quite ugly to read due to the option encoding:

val some: 'a -> ('a -> 'b) -> ⊤ -> 'b
val none: ⊤ -> ({} -> 'a) -> 'a
val map: ('a -> 'b) -> (({head: 'a, tail: 'c} -> ({head: 'b, tail: 'd} -> 'e) -> ⊤ -> 'e) -> (⊤ -> ⊤ -> ({} -> 'f) -> 'f) -> 'd) as 'c -> 'd
val lst: ({head: int, tail: ⊤ -> ({} -> 'a) -> 'a} -> 'b) -> ⊤ -> 'b
val addLst: (({head: int, tail: 'a} -> 'b) -> ({} -> 'b) -> 'b) as 'a

In a practical language, we'd provide algebraic data types (so no need to encode them) and type synonyms to reduce the verbosity of complicated types still.

For the record, here is the example in another prototype I made (whose source is currently private) which handles data types in a more first-class way:

let rec map = fun f -> fun ls -> match ls with
    Cons{head = h; tail = t} -> Cons{head = f h; tail = map f t}
  | Nil{} -> Nil{}

let lst = Cons{head=1; tail=Nil{}}
let addLst = map succ lst

val map: ('a -> 'b) -> (Cons{head: 'a, tail: 'c} ∨ Nil{}) as 'c -> (Cons{head: 'b, tail: 'd} ∨ Nil{}) as 'd
val lst: Cons{head: Int, tail: Nil{}}
val addLst: (Cons{head: Int, tail: 'a} ∨ Nil{}) as 'a

[metaleap]

For the record, here is the example in another prototype I made (whose source is currently private) which handles data types in a more first-class way

I notice it's still private 3 years on — is this proprietary, did it not pan out, or was it at some point anyway merged into the simple-sub code-base?

[LPTK]

The only reason it's private is that the source code is quite unpolished and not ready for the general public :^)

But this old implementation is obsolete. It is completely subsumed by MLstruct, the language for which you opened hkust-taco/mlstruct#2.

[metaleap]

It is completely subsumed by MLstruct, the language for which you opened hkust-taco/mlstruct#2.

Oh yeah, that (MLstruct) might be next for me (after Simple-Sub), only stumbled upon Simple-Sub slightly after MLstruct — and I'm glad to have found it, a better starting point for me: smaller and the paper walks me through an actual real source code implementation; big fan of that work!