On 2018-03-08 05:40, Alexander Tchitchigin via fstar-club wrote:
> Unfortunately, this particular code doesn't work, most likely I
> should've formulated it differently.
You're just missing an open FStar.Mul, AFAICT :)
I didn't answer at first because I was a bit confused by the OP's request; as I
read it, the spec would be something like this:
let foo (l: list int) : (m: list int{m = map (fun x -> x + 2) l}) =
map (fun x -> x + 2) l
(but then of corse the spec is the implementation ^^).
In any case, the answer is that yes, F* can express arbitrary input-output
relations as refinements.
Clément.
> Anyway, you can check the tutorial https://fstar-lang.org/tutorial/
> and study Quicksort example to learn how to specify properties of list
> elements.
>
> As to Smart-contracts and Dependent Types there's already at least one
> paper on the topic: https://iohk.io/research/library/#2F7S5KKZ
>
> Cheers,
> Alex.
>
>
> On Tue, Mar 6, 2018 at 6:20 PM, Will White via fstar-club
> <fstar-club@lists.gforge.inria.fr> wrote:
>> Hi,
>>
>> Rather than trying to find it in the tutorial, I thought I'd ask here about
>> what makes F* unique. I read in Type-Driven Development with Idris that F*
>> uses “refinement types, which are types augmented with a predicate that
>> describes properties of values in that type.” This sounds like what I'm
>> looking for.
>>
>> Idris can specify the length of a vector, Vect 3 Int, but I don't think it
>> can specify anything about the values of its elements, other than their type
>> (e.g. Int). Can F* specify, in the type, that values in a list output by a
>> function are say 2 more than values in the input list?
>>
>> I'm interested in languages like Idris and F* for their potential
>> application to smart contract development.
>>
>> Will
>> _______________________________________________
>> 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
