3 ms·
That's not really dependent typing. All of your examples are attainable without dependent types. data NEL a = NEL a [a] nel :: [a] -> Maybe (NEL a)
by tel 12y ago
That's not really dependent typing. All of your examples are attainable without dependent types.
data NEL a = NEL a [a]
nel :: [a] -> Maybe (NEL a)
nel [] = Nothing
nel (a:as) = Just (NEL a as)
data EqLen a b = EqLen [a] [b]
unzip :: [(a,b)] -> EqLen a b
unzip [] = EqLen [] []
unzip [(a, b):rs] =
let EqLen as bs = unzip rs
in EqLen (a:as) (b:bs)
A dependently typed language can of course do these things (the most popular of them are strict supersets of HM languages after all) but generally they would use dependent types to construct richer and more flexible typing invariants.
- skybrian 12y agoWell sure, that was my point. It seems like, even without dependent types, you could do a runtime check to prove anything you like in a type's constructor, and then other code can rely on it being true. But that doesn't mean it's practical to introduce a new type for every possible assertion, nor is the compiler assisting you very much with your proof.
- tel 12y agoIt's obviously a tradeoff, but dependent types can make the space of these assertion types more rich and also ensure that they are true by construction.