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
Replying to
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
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 wonder if you keep a journal of your general thoughts on the tradeoffs incurred in making a language dependently typed? With how the language is evolving and your vision, what do you think of bringing dependent typing onboard?
1
Sadly most of this is scattered around, eg:
- github.com/pikelet-lang/p
- app.element.io/#/group/+pikel
- gist.github.com/brendanzab/eba
- reddit.com/r/ProgrammingL
I was playing with Roam, but I'm now having a go at using Neuron for my personal note, which I hope will be more future proof?
1
1
Show replies