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`
}
2
1
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!
Replying to
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. 😬