Can't write a prepend / concatenate function

[duvenaud]

I'm trying to prepend an element to sequence in such a way that I can iterate over them together, but

1. I'm not sure which of 3 approaches is most "Dex"y, and
2. None of those three approaches works right now.

Approach A: using product types

v = Fin 4
l = [3@v, 2@v, 3@v, 2@v]   -- The list
blank = 0@v           -- The thing I want to prepend

def prependA (m:Type) ?-> (v:Type) ?-> (blank:v) (seq: m=>v) : (v & m=>v) =
  (blank, seq)

s3 = prependA blank l
:p s3
(0@(Fin 4), [3@(Fin 4), 2@(Fin 4), 3@(Fin 4), 2@(Fin 4)])

So far so good! But I don't know how to iterate over this whole collection with a flat for loop:

:p for k. s3.k
Type error:
Expected: (a=>b)
  Actual: ((Fin 4) & ((Fin 4)=>(Fin 4)))
(Solving for: [a:Type, b:Type])

:p for k. s3.k
          ^^

Approach B: using dependent types

def prependB (n:Int) ?-> (blank:v) (seq: (Fin n)=>v) : (Fin (1 + n))=>v =
  for i. select (i == 0) blank blank  -- ignore implementation for now

which gives:

Type error:Can't reduce type expression: Fin (+) 1 n

def prependB (n:Int) ?-> (blank:v) (seq: (Fin n)=>v) : (Fin (1 + n))=>v =
                                                       ^^^^^^^^^^^^^^^^

Approach C: using sum types

I tried

def prependC (m:Type) ?-> (v:Type) ?-> (blank:v) (seq: m=>v) : (Unit|m)=>v =
  for idx. case idx
    Left () -> blank
    Right i -> seq.i

s3 = prependC blank l

crashed with

Not implemented Unit
CallStack (from HasCallStack):
  error, called at src/lib/Embed.hs:567:8 in dex-0.1.0.0-WMAsfoEK61B3EtpA608ix:Embed

[apaszke]

I'd say that the sum-type based implementation is the one I'd go with. We even have an example for that in eval-tests.

The implementation of sum types is a little bit incomplete, but your program fails only because Unit is not a valid index set (we should probably make it so, because there's no reason not to). Replacing Unit with Fin 1 in the return type seems to allow the program to compile.

The bad error message is likely due to the type-class membership checking being busted after the recent "dependenter" refactor. cc @dougalm

[apaszke]

Ok, I've just pushed a commit that should get your approach C to work. I'm getting this now:

s3 = prependC blank l
s3
> [0@(Fin 4), 3@(Fin 4), 2@(Fin 4), 3@(Fin 4), 2@(Fin 4)]@(Unit | (Fin 4))

[duvenaud]

Wow, thanks for the quick turnaround! I'll give it a try.

[duvenaud]

That works, thanks! But prepending to a product type gives another crash.

def interleave (m:Type) ?-> (v:Type) ?-> (blank:v) (labels: m=>v) : (m & (Fin 2))=>v =
  grid = for i:m. [labels.i, blank]
  for (i, j). grid.i.j

def prepend (first: v) (seq: m=>v) : (Unit|m)=>v =
  for idx. case idx
    Left () -> first
    Right i -> seq.i

v = Fin 4
seq = [3@v, 2@v, 3@v, 2@v]
blank = 0@v

interleaved = interleave blank seq
prepend blank interleaved

The last line crashes with src/lib/Interpreter.hs:89:48-64: Non-exhaustive patterns in PairVal x _.

Promisingly, if we put those last two lines into a function, it at least pass the type checker:

def prepend_and_interleave (blank:v) (seq: m=>v) : ((Unit | (m & (Fin 2)))=>v) =
  interleaved = interleave blank seq
  prepend blank interleaved

FYI, this function is for the CTC loss, where you need to preprocess "text" to " t e x t " to allow for pauses between sounds.

[apaszke]

Should be fixed now!

[duvenaud]

Works now, thanks! I'm impressed with the type system. When I started writing prepend_and_interleave I had no idea how to even express its type.