Conversation
Oh neat! I'm currently making a dependently typed data description language at - the intension is to describe existing binary data formats, but that is a big challenge, hehe. Trying to chip away at it. I really like the sound of this!
1
5
Using it as a basis for other tooling sounds really cool. :) :)
1
1
> we got bogged down in the type checker.
haaaa! The struggle! I'm implementing it directly in Rust, but it often feels cumbersome and slow. I do wonder if I would have been better served making more prototypes.
2
1
yeah the challenge is basically that most of the people who understand dependent type checkers are mathematicians rather than programmers. so all the explanations of it are, um, abstract.
3
4
Agreed. Fortunately we understand unification, but there's really no on-ramp for anyone from a computer science background to learn about it easily.
1
1
What should I be on the lookout for to avoid this fate? And what is the distinction that you missed - was it between first order unification and higher order unification?
1
Tbh I'm not sure I'm following, and would love some more elaboration! Could you be clearer on what the distinction was that you needed to make?
So e.g.:
const : a -> b -> a
const a _ = a
is implicitly quantifying over the types a and b. writing {…} for implicit bits, and ? for the bits we don’t know syntactically, we get:
const : {a : ?} -> {b : ?} -> a -> b -> a
const {_} {_} a _ = a
1
1
10
Show replies