I stepped back to solve a simpler problem: an identity function on
records using fold.
fun identity [ r ::: {Type} ] (record : $r) : ($r) =
fold [ fn t => $t ] (fn [nm ::_] [ v::_] [r::_] [[nm]~r] v => fn
acc => ({nm = v} ++ acc )) () record
but the compiler complains that I have too much arguments for the step function:
cellPull.ur:6:24-6:97: Unification failure
Expression:
fn nm :: Name =>
fn v :: Type =>
fn r :: {Type} =>
fn v : $r => fn acc : $<UNIF:D::{Type}> => {nm = v} ++ acc
Have con:
nm :: Name ->
v :: Type ->
r :: {Type} ->
[[nm = ()] ~ r] =>
($r -> ($<UNIF:D::{Type}> -> $(([nm = $r]) ++ <UNIF:D::{Type}>)))
Need con:
nm :: Name ->
v :: Type ->
r :: {Type} -> [[nm = ()] ~ r] => ($r -> $(([nm = v]) ++ r))
Incompatible constructors
Con 1:
($<UNIF:D::{Type}> -> $(([UNBOUND_REL2 = $r]) ++ <UNIF:D::{Type}>))
Con 2: $(([UNBOUND_REL2 = UNBOUND_REL1]) ++ r)
cellPull.ur:6:4-6:100: Unification failure
Expression:
fold[[Type]] [(fn t :: {Type} => $t)]
(fn nm :: Name =>
fn v :: Type =>
fn r :: {Type} =>
fn v : $r => fn acc : $<UNIF:D::{Type}> => {nm = v} ++ acc) {}
[<UNIF:I::{Type}>] _
Have con: $<UNIF:I::{Type}>
Need con: (<UNIF:J::Type> -> <UNIF:K::Type>)
Incompatible constructors
Con 1: $<UNIF:I::{Type}>
Con 2: (<UNIF:J::Type> -> <UNIF:K::Type>)
Why does it tell this? A proper step function should take the value
and the accumulator as arguments, but the "need con" section tells
that fold does not expect that. Or am I misunderstanding the error
message?
- Gergely
_______________________________________________
Ur mailing list
[email protected]
http://www.impredicative.com/cgi-bin/mailman/listinfo/ur
