Returning a dependent pair from a foreign function

Question

I have the following Chez support file:

(define list-copy-with-length (xs)
  (cons (length xs) (list-copy xs)))

and I have this Idris file:

%foreign "scheme,chez:list-copy-with-length"
prim__listToVect : List t -> (Nat, Vect n t)

listToVect : List t -> (n ** Vect n t)
listToVect ls =
  let (n, vs) = prim__listToVect ls
  in MkDPair n vs

Naturally, type-checking fails on this code, because the compiler does not know that the n defined in the let expression is the same as the n in the return type of listToVect.

I tried a few guesses at using believe_me to fix this, but I wasn't able to figure it out. Is it possible to define a function like this? What is the correct way to do it, without incurring significant runtime cost of recursively re-computing the length (as in Data.Vect.filter)?

Here is one such guess:

listToVect : {t : _} -> {n : _} -> List t -> (n ** Vect n t)
listToVect ls =
  let (n', vs) = prim__listToVect ls
      itsEqualDamnit : Equal n' n = believe_me ()
  in rewrite itsEqualDamnit in MkDPair n vs

Ideally I'd like to entirely avoid unpacking the pair anyway, because (at least in the Chez backend), pairs and depdendent pairs are both represented identically as cons cells.

Answer 1

believe_me is already an unsafe cast. Just... cast the Vect?

%foreign "scheme,chez:list-copy-with-length"
prim__listToVect : List t -> (Nat, Vect n t)

listToVect : List t -> (n ** Vect n t)
listToVect ls =
  let (n, vs) = prim__listToVect {n = 0} ls
  in  MkDPair n (believe_me vs)

Your Scheme code is wrong: define's syntax is not like that and list-copy-to-vect needs three arguments, since prim__listToVect has three arguments (t, n, and a List t). Note that I pass a dummy in for n on the Idris side.

(define (list-copy-with-length t n xs) (cons (length xs) (list-copy xs)))

You can be even more direct by pairing this Scheme definition

(define (idris-prim-listToVect t xs) (cons (length xs) (list-copy xs)))

With this Idris

%foreign "scheme,chez:idris-prim-listToVect"
prim__listToVect : List t -> (Nat, List t)

listToVect : List t -> (n ** Vect n t)
listToVect xs = believe_me (prim__listToVect xs)

(This works since, as you noted, a DPair is represented the same as a normal pair and List is represented the same as a Vect.)