Having seen this answer about the elements of a List that depend on the type of preceding elements , where the problem was solved with the following list definition:
type ('a,'b) mlist =
| MNil : ('a,'a) mlist
| MCons : ('a, 'b) element * ('b,'c) mlist -> ('a,'c) mlist
where an "element" is :
module Tag = struct
type root = Root
type fruit = Fruit
(* ... *)
end
type (_,_) element=
| Fruit : (Tag.root, Tag.fruit) element
| Veggie : (Tag.root, Tag.veggie) element
(* ... and so on *)
I find it really useful for creating a list where you want to have some rules about the order of elements. For example when creating a list of layers in a neural network...
I now want to reverse this list. So I have defined a new reversed list type like this:
type ('a,'b) rev_list =
| RNil : ('a,'a) rev_list
| RCons : ('b, 'c) element * ('a,'b) rev_list -> ('a,'c) rev_list
where the last element's type depends on the previous one.
But I have a trouble with the reverse function :
let rec rev : type a b c. (a, c) mac_list ->
(b, a) rev_list ->
(c, b) rev_list =
fun lst acc ->
match lst with
| MNil -> acc (* <- error *)
| MCons (h, t) ->
revp t (RCons (h, acc))
Obviously, Ocaml complains that the return type does not match the type of accumulator: type (b, a) is not compatible with type (c, b) ...
However if I write (b, a) rec_list as a return type, I get an error on the last line (on recursive function call) because, obviously, the type of the previous list element in the acc is not the same as the one that I add right now.
And I don't think I can use any existential wrappers here as (afaik) I would lose the type information about list elements...
Although the code is in Ocaml I would be happy if you have a solution in Haskell or at least some advice where can I search for it..
If you have any idea on how it is possible to restrict the order of elements in a list or maybe some other data structure, knowing that I also need to iterate through it backwards, I would be grateful to know.
EDIT:
Looks like I oversimplified the problem to post it here, my bad.
But what if the original problem looks like this:
I actually have mlist and rev_list defined like so:
type ('a,'b) mac_list =
| MNil : ('a,'a) mlist
| MCons : ('a, 'b) element * (('b,'c) element, _) mlist ->
(('a,'c) element, 'e) mlist
type ('a,'b) rev_list =
| RNil : ('a,'a) rev_list
| RCons : ('b, 'c) element * (('a,'b) element, _) rev_list ->
(('a,'c) element, 'e) rev_list
I'm not sure if those definitions make sense, but I really need the information about the types inside an "element" to iterate through the list as I want to pass the "fruit" or "vegie" of the current element to the next iteration.
My iteration code which works fine until I want to reverse the list:
(* ... *)
type (_,_) element=
| Fruit : Tag.root -> (Tag.root, Tag.fruit) element
(* ... *)
let rec iter : type a b c. ((a, b) element, c) mlist -> a
-> unit =
fun list input ->
match list with
| MNil -> ()
| MCons (element, tail) ->
(match element with
| Fruit root ->
(* processing the input *)
let fruit : Tag.fruit = (* to fruit *) root + input in
iter tail fruit
(* ... *) )
And the rev function is now as follows:
let rec rev : type a b c d. ((b, c) element, d) mlist ->
((a, b) element, _) rev_list ->
((a, c) element, _) rev_list =
fun lst acc ->
match lst with
| MNil -> acc
| MCons (h, t) ->
rev t (RCons (h, acc))
In this case I keep getting an error on returning an accumulator no matter the order of types...
You are one typo away from the solution,
let's first rewrite the type of your rev function with more explicit types:
let rec rev : type bottom current top.
(current, top) mlist ->
(bottom, current) rev_list ->
(top, bottom) rev_list =
fun lst acc ->
match lst with
| MNil -> acc (* <- error *)
| MCons (h, t) ->
rev t (RCons (h, acc))
If you look closely at the type of the two rev_lists, there is something strange in the order of their parameter: the intermediary list is a (bottom, current) rev_list thus preserving the order bottom -> top at the type system while, the result is a (top, bottom) rev_list which reverse the order of the type parameters.
There is an inconsistency here which is not that surprising since the two choices are valid in function of the definition of rev_list. In your case, you have:
type ('a,'b) rev_list =
| RNil : ('a,'a) rev_list
| RCons : ('b, 'c) element * ('a,'b) rev_list -> ('a,'c) rev_list
whereas the other choice would be
type ('a,'b) rpath =
| RPNil : ('a,'a) rpath
| RPCons : ('b, 'a) element * ('b,'c) rpath -> ('a,'c) rpath
Notice that your choice preserves the direction of the element of the list whereas the second one reverse it.
Thus you have chosen at the start that the reverse of ('a,'b) mlist will be ('a,'b) rev_listand not('b,'a) rev_list`.
In other words, to fix your function we just need to remember this choice consistently and make the return type (bottom,top) rev_list rather than
(top,bottom) rev_list:
let rec rev : type bottom current top.
(current, top) mlist ->
(bottom, current) rev_list ->
(bottom, top) rev_list =
fun lst acc ->
match lst with
| MNil -> acc
| MCons (h, t) ->
rev t (RCons (h, acc))