Attempt to write to file produces llvm undefined ref error

[adam-antonik]

I'm trying to write structured data to a file. The below looks like it might work from the types but causes "Fatal error: Internal error, reference to undefined variable: .t17844.rv0" when run through hi.

x :: [int] -> ()
x d = let f = (writeFile("test1") :: ((file) _ {vs:[int]@?})) in f.vs <- store(d)

[kthielen]

Not the greatest error message, but the short story is that we use these files like extensions of the environment -- so they work differently as global variables, and reference types get resolved through them to depend on the files they index into (a limited form of dependent type).

We could use better syntax around this, but you can get a file like this with:

$ hi -s
> f = writeFile("./file.db") :: ((file _ {xs:[int]@?}))
> f.xs <- unsafeCast(storeAs(f,[1..1000000]))                                                      
> f.xs
[1, 2, 3, 4, ...

[adam-antonik]

Thanks. It seems that if I want to store a series, and append to it like this, I probably shouldn't choose an array. What would be the efficient solution here?

(I also just tried to store a list in the say way, but storeAs complains about constraints

f = writeFile("./file2.db") :: ((file _ {xs:^x.(() + (int * x))@?}))
f.xs <- unsafeCast(storeAs(f, foldr(cons, nil(), [1..10])))
stdin:1,1-59: Failed to compile expression due to unresolved type constraint
StoreAs { xs:^x.(() + (int * x))@? } ^x.(() + (int * x)) a
)

[kthielen]

Right, the array type requires that a definite length is given, so if you want to store data without a definite length then you need a different type. One approach taken in the fregion.H C++ code is to store a sequence of T as ^x.(()+([T]@?*x@?)@?, ie as a (stored) linked list of (stored) arrays. This is a handy compromise for our use-cases because we can compute results very quickly for contiguous data in arrays.

We don't usually do the producer side from hobbes, so this is a little awkward from neglect, but it could be cleaned up with a little bit of syntax.

Basically, here's one way to do what you're describing:

$ hi -s
> f = writeFile("./file.db") :: ((file _ {xs:(^x.(()+([int]@?*x@?)))@?}))

> f.xs <- store(roll(|0=()|))

That gets you initialized to an empty list of batches, and then you can build up from there:

> f.xs <- store(roll(|1=(unsafeCast(storeAs(f,[1..1000])), f.xs)|))
> f.xs <- store(roll(|1=(unsafeCast(storeAs(f,[1001..2000])), f.xs)|))

> countBy(\x.x%10, f.xs[0:])
0 200
1 200
2 200
3 200
4 200
5 200
6 200
7 200
8 200
9 200