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.
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> 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
> 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
