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
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
Eg. it would be nice to have:
record {
A = U32,
len = 3,
data = ["a", "b", "c"],
} : Record {
A : Type = U32,
len : A,
data : Array len String,
}
1
I think if you had some sort of singleton type with subtyping+coercions you might be able to do that, kind of like in that paper? But some folks find this solution a bit distasteful I think? github.com/pikelet-lang/p 🤔
This is the relevant bit of the paper, introducing 'intentional manifest fields', and how they are elaborated:
