You can't simply elaborate your program to a record term and a record type - you need to be able to check the record type while also knowing some of the definitions in the record term.
Conversation
For example this signature:
pub A : Type,
pub A = U32,
pub len : A,
len = 3,
pub data : Array len String,
data = ["a", "b", "c"],
1
1
cannot be elaborated to the following record:
record {
A = U32,
len = 3,
data = ["a", "b", "c"],
} : Record {
A : Type,
len : A,
data : Array len String,
^^^ error: expected `U32`, found `A`
}
2
1
I think this error is fine…seems like the issue is that signatures aren’t explicit about which types are opaque/existential. You need to know which U32s to pack as As and which to leave alone (or which As to inline as U32). So why not require e.g. ‘Vector (pub len) String’ here?
1
That is, it seems analogous to a situation like this expression:
pack { Int, (1, 2) }
Which is missing a signature to specify which Ints to pack and which to leave alone:
as ∃t. t × Int
So the compiler is doing something like (erroneously) guessing ∃t. t × t.
1
Or do you want to retain the fact that the vector’s length is determined by ‘len’, while also preventing the use of ‘len’ as a U32 elsewhere? (That is, a user *knows* it must be a U32, but cannot *rely* on that fact.) That seems…subtly dependent (ha) on scope, but feasible, idk
1
Yeah, I'd like to retain that - perhaps the example is not super clear. There are other places where this pops up, like in cs.rhul.ac.uk/~zhaohui/Modul:
2
I see. It does seem like there ought to be a tidier solution than introducing implicit coercions like that, yeah. In a way I guess you need to distinguish ‘U32’ from “some type ‘A’ which is equal to ‘U32’”…
1
1
…in such a way that ‘Vector len String’ is somehow aware that whoever put ‘len’ *in* there must have had a proof that A=U32, but nobody can take it back *out*.
1
1
I do wonder how other dependently typed languages handle with this. Do they prevent you from leaking out implementation details accidentally in signatures, or do they substitute the definition at each usage site?
1
Might need to read the docs on Agda's `private` and `abstract` keywords again: agda.readthedocs.io/en/latest/lang
> Inside abstract blocks, abstract definitions reduce while type checking definitions, but not while checking their type signatures. Otherwise, due to dependent types, one could leak implementation details (e.g. expose reduction behavior by using propositional equality).
1
This looks a bit concerning? It seems like `Child.y` is leaking out of the module? 🤔
