Re: [fstar-club] Dependent record field types

[Jannis via fstar-club]

Hello Santiago,

thanks a lot! Using inductive types solved my problem.

Regards,
Jannis


On Mon, May 15, 2017 at 12:38, Santiago Zanella wrote:

Hi Jannis,

Currently, F* doesn't allow you to define records with fields whose types are dependent on the values of other fields. This is a known restriction and there is an open request for extending the language to support this: https://github.com/FStarLang/FStar/issues/801 <https://github.com/FStarLang/FStar/issues/801>.

The workaround is to use an inductive type with a single constructor. I believe the result is very similar to what records are desugared to.

Following your example, you could write instead

```
noeq type theType =
  | MktheType:
     min: int ->
     max:int ->
     func: (x:int{x >= min && x <= max} -> Tot int) ->
     theType
```

Note that using a record type, like `theTypeNoRestrictions` allows you to write succinct updates using `with` syntax:

```
noeq type theTypeNoRestrictions = {
        min: int;
        max: int;
        func: (int -> Tot int);
}

let x: theTypeNoRestrictions =
  { min = 0; max = 0; func = fun n -> n }

let y: theTypeNoRestrictions =
  MktheTypeNoRestrictions 0 0 (fun n -> n)

let f (x:theTypeNoRestrictions) =
  { x with min = 0 }

let g (x:theTypeNoRestrictions) : int =
  x.mineTypeNoRestrictions) : int =
  x.min
```

Unfortunately, there is no record-like syntax support when you use an inductive type:

```
noeq type theType =
  | MktheType:
     min: int ->
     max:int ->
     func: (x:int{x >= min && x <= max} -> Tot int) ->
     theType

let x: theType =
  MktheType 0 0 (fun n -> n)

(*
// No syntax support for record-like construction and update
let x: theTypeNoRestrictions =
  { min = 0; max = 0; func = fun n -> n }

let f (x:theType) =
  { x with min = 0 }
*)

let g (x:theType) : int =
  x.min
```

Cheers,
--Santiago

On Mon, May 15, 2017 at 9:04 AM, Jannis via fstar-club <fstar-club@lists.gforge.inria.fr <mailto:fstar-club@lists.gforge.inria.fr>> wrote:

    Hello,


    I wanted to ask whether it is somehow possible to restrict the
    type of a field inside a record according to values inside of the
    record itself.

    Example:

    noeq type theTypeNoRestrictions = {
            min: int;
            max: int;
            func: (int -> Tot int);
    }

    noeq type theType = {
            min: int;
            max: int;
            func: (x:int{x >= min && x <= max} -> Tot int);
    }

    If this is not possible yet, are there any alternatives or
    workarounds? It doesn't even have to be a record, I only want to
    access the values of "min", "max" and be able to call the function
    "func".

    The motivation behind this is, that I want to use elements with a
    type t similar to "theType" as a parameter for some functions f. I
    am currently using a record because I need access to all the
    fields of t inside these functions. Also I want to prove some
    post-conditions of f, which is why I need to restrict t.

    In reality, the intended type of "func" looks more like this
    func: (x:int{x >= min && x <= max} -> Tot (z:int{something z})
    but was simplified in the example above because "something z" does
    not directly depend on "min" or "max".

    I really appreciate any help you can provide.

    Regards,
    Jannis**

    _______________________________________________
    fstar-club mailing list
    fstar-club@lists.gforge.inria.fr
    <mailto:fstar-club@lists.gforge.inria.fr>
    https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
    <https://lists.gforge.inria.fr/mailman/listinfo/fstar-club>

_______________________________________________
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club