List with internal type processing

Learning
#1

Hi,

type _ spec =
  | [] : 'a spec
  | (::) : (string * (unit -> 'state) * ('proto -> 'state -> 'payload)) * (string * (unit -> 'state2) * ('proto -> 'state2 -> 'payload)) spec -> (string * (unit -> 'state -> 'state2) * ('proto -> 'state -> 'state2 -> 'payload)) spec

So it is a list of identifiers (string), a internal state production function (unit -> 'state) and a function which takes some input data (same for every list entry), its specific state and produces a an output data (same for every list entry) ('proto -> 'state -> 'payload). I can get it sort of to type but I don’t know how to write a function to process these. I’m not even sure my ‘::’ implementation is actually correct because I am still confused on how GADTs work.

#2

What are you trying to model?

You have explained how you want to process your list, but so far, you could just do that with a bunch of folds and some high order functions. GADTs are needed when you want to manipulate that as data, and that doesn’t seem needed here unless you have some specific usage in mind.

#3

I am not sure what you intend to do with this type. In general with GADTs, it is useful to have in mind which functions are supposed to consume the type-level information produced by the GADT definition.

For instance, if the aim is to write a function

let rec to_payload proto = function
 | [] -> []
 | (_name, producer, output) :: q -> output proto (producer () :: to_payload proto q

where the state produced by producer varies from element to element, the easiest solution is not to use heteregeneous list, but to pair the producer and output function using an existential quantification on the
shared state:

type ('proto, 'payload) arrow =
    X : { producer : unit -> 'state; output : 'proto -> 'state -> 'payload;
    } -> ('proto, 'payload) arrow
let apply (X {producer;output}) proto = output proto (producer ());;

The previous function then becomes:

let rec to_payload proto = function
 | [] -> []
 | (_name, x) :: q -> apply x proto :: to_payload proto q

But then, it is even simpler to replace the (x,y) arrow type by the closure fun proto -> output proto (producer ()).

Consequently, without more detail, it is hard to even tell if GADTs are needed in your design.

#4

You are both right, I supplied too little detail and GADTs might be the wrong thing to do here.

I think @octachron’s arrow is going very much in the direction of it.

So, the idea is that I have different identifiers (strings) which go into different processing pipelines. Each of those has a different initialization (like setting up connections) that is invoked when the list of pipelines is processed. That result is then saved (maybe using a curried parameter) and whenever I get a value I would pick the correct one from the list it would just pass it through.

So in code it would look sort-of like this:

let setup_pipelines xs =
  List.map (fun (name, init, process) ->
    let state = init () in
    let v = process state in
    (name, v)) xs

This yields ('a * (unit -> 'b) * ('b -> 'c)) list -> ('a * 'c) list as signature, but this requires all the 'b to be the same. At this point I could make an ADT but since these 'b are not meant to be used anywhere else than as the output of init and the input to process I am hoping for a way to specify that whatever the 'b is it just has to be the match the types that the initializer returns and producer expects.

#5

Why do you need init and process to be separated? You only use them together here. You could just store fun x -> process (init ()) x for each list element, and apply that. The 'b is hidden inside the closure, without any type shenanigan.

1 Like