why do ML programmers put up with this endless sea of ".t".
Conversation
twitter.com/glaebhoerl/sta
(if you know of a nice way to resolve this I am very interested)
Quote Tweet
1. conflating types with modules is Wrong
2. ML's `Foo.t` idiom is unsightly
3. Haskell's `import Data.Map.Map` idiom is unsightly
me: 
1
2
(which two syntaxes do you mean? . and ::?)
Rust does conflate types and modules, aka `impl` blocks and "UFCS"
1
1
It's kiiind of neat from an ergonomics perspective. Less names to come up with. Lean is interesting - each type adds a new namespace that you can add stuff to. Not sure how it works out though. Personally I prefer just going with modules==records though.
3
Modules ~= records is the only correct way to go, IMO, at least conceptually (if we can work out some foundational issues around impredicative universe polymorphism, anyway). You do want other stuff from modules but you hope it can desugar to records.
1
> some foundational issues around impredicative universe polymorphism
Could you elaborate on those?
If you have universe polymorphic constants in a functor, you get a type signature with non-prenex universe polymorphism. It's *probably* fine, but there's no set model for it yet and (in Coq anywayt) no syntax, either, precluding records as modules. Hopefully, that'll change!
1
1
Would this show up much in general programming? For context I'm working on a dependently typed programming language that uses dependent records for modularity: github.com/brendanzab/pik - less of a focus on theorem proving right now though.
1
Show replies