Trying to avoid having top level commands in my dependently typed language. It's frustrating that you can't give a type to a signature easily! You need manifest fields or singletons or identity type trickery to make certain definitions public, or else you limit expressiveness. 🤔
Conversation
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.
1
1
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`
}
Replying to
Been looking at some Zhaohui Luo's past papers on records and manifest fields which seem relevant, but I'm still trying to see how other languages handle it. Signature privacy definitely seems pretty finicky in dependently typed languages. Curious if anyone has more pointers!
1
1
Loving these BIG record types. Why can't I have an editor that does this?
From “Dependent Record Types Revisited” by Zhaohui Luo: doi.org/10.1145/173581
3
2
7
Remembered that Agda has manifest fields defined as a library!
• agda.github.io/agda-stdlib/RE
• agda.github.io/agda-stdlib/Da
Seems to be based on “Dependently Typed Records in Type Theory” by Robert Pollack: link.springer.com/article/10.100 🤔
1
1
Like, this kind of suggests that I might not _have_ to build singletons into my core type theory? But I might still need to do subtyping somehow, which could make type inference more painful. 😬
Replying to
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
Show replies