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!
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
Seen Alfa/Agda 1? There was an editor that does that.
1
