Hi Will,
Actually, both Idris (and any Dependently-Typed language) and F* (or
LiquidHaskell for that matter) can express properties of elements. I
implemented your example in Idris, it goes like this:
```
module Example
import Data.Vect
ix2 : Int -> Int
ix2 i = i*2
foo : {n: Nat} -> (l: Vect n Int) -> (m: Vect n Int ** ((x: Int) ->
Elem x l -> Elem (ix2 x) m))
foo {n} l = (m ** prf)
where
m : Vect n Int
m = map ix2 l
prf : (x: Int) -> Elem x l -> Elem (ix2 x) m
prf x xInL = mapElem {f = ix2} xInL
```
I define `2*x` as a named function because otherwise function
extensionality is needed to prove anonymous ones all are the same.
In F* it should be something like
```
module Example
open FStar.List.Tot
let ix2 (i:int) = i*2
val foo : l:list int
-> Tot (m:list int{forall (i:int). mem i l <==> (exists (i2:int). mem
i2 m /\ (i2 == ix2 i))})
let foo l = map ix2 l
```
Unfortunately, this particular code doesn't work, most likely I
should've formulated it differently.
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
