Doubly-dependent record field

[wkolowski]

Hello

What is the best way to achieve this:

type t =
{
    a : bool;
    b : (if a then bool else unit);
    c : (if a then (if b then string else unit) else unit);
}

I know it's possible to just factor out the common if a then ... else ... into a separate record, like below, but can this factoring out be avoided with a nice, inline solution?

type aux =
{
    b : bool;
    c : (if b then stirng else unit);
}

type t =
{
    a : bool;
    bc : (if a then aux else unit);
}

In Coq this thing is simple, you can just do a double match:

Record t : Type :=
{
    a : bool;
    b : if a then bool else unit;
    c :
      match a, b with
          | true, true => string
          | _   , _    => unit
      end;
}.

[W95Psp]

Hi,

I think your first definition doesn't work because F* does not even try to unify the type of the condition passed to the if _ then _ else _ combinator with bool, it just expects "plain" bool.

You could just wrap your b into the identity function for instance (the code below works) so that F* actually try to unify the type of your field b with bool. id will more or less yield a proof obligation (if a then bool else unit) <: bool that is easily discharged by normalization/unfolding.

type t =
{
    a : bool;
    b : (if a then bool else unit);
    c : (if a then (if id b then string else unit) else unit);
}

[nikswamy]

An even more explicit version:

let dep (b:bool) (t: (_:unit{b} -> Type))
                 (f: (_:unit{~b} -> Type)) 
    = if b then t() else f()
let as_t #b #t #f (x:dep b t f{ b }) : t() = x
let as_f #b #t #f (x:dep b t f{ ~b }) : f() = x

type t =
{
    a : bool;
    b : dep a (fun _ -> bool) (fun _ -> unit);
    c : dep a (fun _ -> dep b (fun _ -> string) (fun _ -> unit))
              (fun _ -> unit)
}

[nikswamy]

But you make a good point. The version that you wrote originally with the match on the tuple could be made to work with some tweaks to type inference ... will try.