The Author Online Book Forums are Moving

The Author Online Book Forums will soon redirect to Manning's liveBook and liveVideo. All book forum content will migrate to liveBook's discussion forum and all video forum content will migrate to liveVideo. Log in to liveBook or liveVideo with your Manning credentials to join the discussion!

Thank you for your engagement in the AoF over the years! We look forward to offering you a more enhanced forum experience.

In the implementation for getPrefix in section 11.1.4 in step 4, you show the following hole:

  a : Type
  k : Nat
  value : a
  xs : Inf (InfList a)
--------------------------------------
getPrefix_rhs_1 : List a


… and finish the implementation with the clause

getPrefix (S k) (value :: xs) = value :: getPrefix k (Force xs)


However, this is not what I'm seeing in Idris 0.99. The Inf has already been removed and I don't need a Force:

- + Main.getPrefix_rhs_1 [P]
 `--                     a : Type
                         k : Nat
                     value : a
                        xs : InfList a
     ----------------------------------
      Main.getPrefix_rhs_1 : List a


The next section talks about how Idris will implicitly insert Delay and Force for you. Has any of this behaviour changed between 0.12 and 0.99?

Here's the complete code:

data InfList : Type -> Type where
  (::) : (value : elem) -> Inf (InfList elem) -> InfList elem

%name InfList xs, ys, zs

countFrom : Integer -> InfList Integer
countFrom x = x :: Delay (countFrom (x + 1))

getPrefix : (count : Nat) -> InfList a -> List a
getPrefix Z _ = []
getPrefix (S k) (value :: xs) = ?getPrefix_rhs_1
In section 11.1.4, we're implementing the function getPrefix : (count : Nat) -> InfList ty -> List ty.

A (very) minor nitpick: the type variable changes from ty to a when showing the implementation below. smilie
V13, section 8.6.2:

“By using Dec, you’ve been able to write explicitly in the type what checkEqNat is supposed to do: run either a proof that the inputs are equal, or a proof that they’re not.”


Should this be “return either a proof […]”?
Turns out that my own Vect definition was wrong… Sorry for the noise. smilie
(MEAP v12, Idris 0.12.3)

In exercise 8.2.6.2, if I type in the skeleton definition in the book:

my_reverse : Vect n a -> Vect n a
my_reverse xs = reverse' [] xs
  where
    reverse' : Vect n a -> Vect m a -> Vect (n+m) a
    reverse' acc []        = ?revPrfNil acc
    reverse' acc (x :: xs) = ?revPrfXs (reverse' (x :: acc) xs)


… I don't get the nice listing of holes, but instead the following error:


     When checking left hand side of Main.my_reverse, reverse':
     Type mismatch between
             Vect {a = Type} (S k) a (Type of x :: xs)
     and
             Vect {a = ty} (S k) a (Expected type)
     
     Specifically:
             Type mismatch between
                     Type
             and
                     ty


After some fumbling around, I found a way to make the error go away, but I don't really know why this works, nor what the original error meant.

my_reverse : {a : Type} -> Vect n a -> Vect n a
my_reverse xs = reverse' [] xs
  where
    reverse' : {a : Type} -> Vect n a -> Vect m a -> Vect (n+m) a
    reverse' acc []        = ?revPrfNil acc
    reverse' acc (x :: xs) = ?revPrfXs (reverse' (x :: acc) xs)


Is this expected behaviour here? Did I do something wrong?
In V03 chapter 2 you write “This begs the question: when is it a good idea to use the qualified style (with the module name prefixed) over the unqualified style?”. While I know that “begging the question” colloquially means “raising the question” instead of its original meaning from logic, you'll save yourself two angry emails if you change it to “raises the question”. smilie
In the note ‘IO in Haskell and Idris’, in the setence ending with ‘you can safely move on to Section   “Reading and Validating Dependent Types”’, the link takes me to the start of chapter 5. I'm using the epub verision in iBooks.
I also see this error with version 0.9.20.
I'd also like to learn more about this.

A couple of things I can think of:

- Not possible(?) to do full type inference à la ML
- Need to define types and functions before use, so ordering is important and `mututal` blocks are needed when function a calls function b which calls function a again.