translating Fin type in Haskell

[Zilin Chen]

Dear LH folks,

I just started learning a bit LH and encountered a problem:

For the canonical `SNat n', `Fin n' and `Vec n t' type[1], is there a
way to write idiomatic definitions in LH which is equivalent to the
Haskell code below?

```
allInts :: SNat n -> Vec n (Fin n)
allInts SZero = VNil
allInts (SSucc n) = FZero `Cons` (FSucc <$> allFins n)
```

Btw, I also had few unrelated questions.

1. LH prompts that my standard `vlen' measure for `Vec t' type has no
decreasing parameter. I tried `autosize' and `data [vlen] t = ...' but
both failed due to other errors:
```
{-@ measure vlen @-}
{-@ vlen :: a:Vec t -> {l:Nat|l = vlen a} @-}
vlen Nil = 0::Int
vlen (Cons _ as) = vlen as + 1

-- 27 | vlen Nil = 0::Int
-- ^^^^
-- vlen
-- No decreasing parameter

```
Is there a way to prove the measure terminating (or is it needed)?
What's the right way to define it? (Also what I found difficult learning
LH is that there're several ways of
doing the "same" thing, suggested by different tutorials/docs but in
fact they're subtly different.)

2. I have a function which LH fails to verify (and takes a long while to
reject):

```
{-@ splitAt :: n:Nat
-> a:{Vec t|vlen a >= n}
-> {b:(Vec t, Vec t)|vlen (snd b) = vlen a - n && n = vlen
(fst b)} @-}
splitAt (0::Int) as = (Nil, as)
splitAt n (Cons a as) = let (b1,b2) = splitAt (n-1) as
in (Cons a b1, b2)

```
I got an error:

```
Error: Liquid Type Mismatch

80 | splitAt (0::Int) as = (Nil, as)
^^^^^^^

Inferred type
VV : ((Vec a), (Vec a))

not a subtype of Required type
VV : {VV : ((Vec a), (Vec a)) | vlen (snd VV) == vlen as - ?a
&& ?a == vlen (fst VV)}

In Context
as : {as : (Vec a) | vlen as >= ?a
&& vlen as >= 0
&& vlen as >= 0}

?a : {?a : Int | ?a >= 0}
```

What makes it unable to prove it? Am I missing something obvious?

Thanks heaps,
Zilin

-----------------------------------------------------------------------

[1] definitions:

data Nat = Zero | Succ Nat

data SNat (n :: Nat) where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)

data Fin (n :: Nat) where
FZero :: Fin (Succ n)
FSucc :: Fin n -> Fin (Succ n)

data Vec (n :: Nat) (t :: Type) where
VNil :: Vec Zero t
VCons :: t -> Vec n t -> Vec (Succ n) t

[Ranjit Jhala]

Dear Zilin,

thanks for your questions!

(The code below is at:

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1479182782_18068.hs

you can play with it there.)

The `Fin` type is simply:

```

{-@ type Fin N = {v:Nat | v < N} @-}

```

You can define the measure `vlen` as:

```

{-@ measure vlen :: Vec a -> Int

    vlen Nil         = 0

    vlen (Cons x xs) = 1 + vlen xs

  @-}

```

and make it the "default measure" for `Vec` as:

```

{-@ data Vec [vlen] a = Nil | Cons {hd :: a, tl :: Vec a } @-}

```

and now, you can define "Vectors of size N" as:

```

{-@ type VecN a N = {v:Vec a | vlen v == N} @-}

{-@ invariant {v:Vec a | 0 <= vlen v} @-}

```

(the "invariant" business is an unfortunate 

artifact of the present implementation, which

I hope will get fixed soon!)

Thus, you can write a `map` function for such 

vectors as:

```

{-@ vmap :: (a -> b) -> xs:Vec a -> VecN b (vlen xs) @-}

vmap :: (a -> b) -> Vec a -> Vec b

vmap _ Nil         = Nil

vmap f (Cons x xs) = Cons (f x) (vmap f xs)

```

and finally, your `allInts` function as:

```

{-@ allInts :: n:Nat -> VecN (Fin n) n @-}

allInts :: Int -> Vec Int

allInts 0 = Nil

allInts n = Cons 0 ((1 +) `vmap` allInts (n - 1))

```

Finally, not sure why you had trouble with 

the `splitAt`; the following works for me:

```

{-@ splitAt :: n:Nat

            -> a:{Vec t|vlen a >= n}

            -> {b:(Vec t, Vec t)|vlen (snd b) = vlen a - n && n = vlen (fst b)} @-}

splitAt (0::Int) as   = (Nil, as)

splitAt n (Cons a as) = let (b1, b2) = splitAt (n - 1) as

                        in (Cons a b1, b2)

```

Are you using an older version of LH?

[Like I said, all of the above code is at the permalink URL

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1479182782_18068.hs]

Can you let me know if this helps? 

Thanks again!

Ranjit.

--
You received this message because you are subscribed to the Google Groups "liquidhaskell" group.
To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskell+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Zilin Chen]

Hi Ranjit,

Thanks a lot for your detailed explanation. Thus I have a few more follow-up questions and observations.

1. When I define `VecN t N`, the value parameter has to come after the type parameter (otherwise I get some seemingly meaningless errors). Is that right?

2. For a same measure, I found 3 different styles of definitions are commonly mentioned.

```
-- (1)
{-@ measure vlen :: Vec t -> Int
vlen Nil = 0

vlen (Cons _ as) = vlen as + 1

@-}

-- (2)
{-@ measure vlen @-}
vlen :: Vec t -> Int
vlen Nil = 0

vlen (Cons _ as) = vlen as + 1

-- (3)
{-@ measure vlen :: v:Vec t -> {a:Int | vlen v = a} @-}
vlen :: Vec t -> Int
vlen Nil = 0

vlen (Cons _ as) = vlen as + 1

```
How do you compare them and what are the use cases for each? From what I can tell, (1) doesn't require termination proof, but the definition of out of Haskell's scope as (2) and (3).
In particular, I was wondering what the self-referential (3) style is for. Also why can't I write {-@ measure vlen :: v:Vec t -> {a:Nat | vlen v = a} @-} instead in (3)? It says "Refinement
Type Alias cannot be used in this context".

3. When using default measure `data Vec [vlen] t = ...`, I have to use record syntax for data constructors, otherwise it gives an incomprehensible error. Is it just
an implementation limitation?

4. I did a bit more experiments and found that the cause of my `splitAt` failure was due to "--higherorder". I didn't know that this flag has some side effects. Is it a bug/feature?
Code is here: http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1479272608_18192.hs

Thanks again,
Zilin

[Ranjit Jhala]

1. When I define `VecN t N`, the value parameter has to come after the type parameter (otherwise I get some seemingly meaningless errors). Is that right?

​Yes, that is right -- the parser is set up to first take the "type" parameters (e.g. `t`) and then the "value" parameters (e.g. `N`) -- the latter need to be upper-case,

due to my inability to write nice parsers...

2. For a same measure, I found 3 different styles of definitions are commonly mentioned.

```
-- (1)
{-@ measure vlen :: Vec t -> Int
vlen Nil = 0
vlen (Cons _ as) = vlen as + 1
@-}

-- (2)
{-@ measure vlen @-}
vlen :: Vec t -> Int
vlen Nil = 0
vlen (Cons _ as) = vlen as + 1

-- (3)
{-@ measure vlen :: v:Vec t -> {a:Int | vlen v = a} @-}
vlen :: Vec t -> Int
vlen Nil = 0
vlen (Cons _ as) = vlen as + 1
```

​

You are right -- if you write (1) then the termination check is disabled. 

If you write (2) then you get to use the measure as a haskell function 

too -- but that is why the termination check gets switched on. 

You should **never** have to write (3).

*Ideally* you would only write (2) -- but the way the implementation 

happened, we first supported (1) -- over time, I expect us to always 

converge to (2) but with the termination checking done "structurally".

3. When using default measure `data Vec [vlen] t = ...`, I have to use record syntax for data constructors, otherwise it gives an incomprehensible error. Is it just
an implementation limitation?

​Yes -- that is an unfortunate implementation limitation! (if you could​ file an issue for it that would be great!)

4. I did a bit more experiments and found that the cause of my `splitAt` failure was due to "--higherorder". I didn't know that this flag has some side effects. Is it a bug/feature?
Code is here: http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1479272608_18192.hs

​Oops! That is *definitely*​ a bug! I am going to file a report, thanks VERY MUCH 

for pointing it out!!!

- Ranjit.