4
$\begingroup$

As we know, dependent type allows programmers to write bugless programs.
But as I know there's only very few languages support dependent type, like Haskell with extensions, Idris, Agda, F*, etc.

Since these are all functional languages, is there any possibility to add dependent type into an imperative language?

I've googled and found some papers like http://www.ats-lang.org/MYDATA/Xanadu-lics00.pdf or https://www.cs.bu.edu/~hwxi/academic/papers/XanaduAbs.ps, but they create their own languages.

Improve this question
$\endgroup$
2
  • $\begingroup$ There has been some work done on this for Javascript. [linkhttp://goto.ucsd.edu/~ravi/research/oopsla12-djs.pdf) $\endgroup$ – jcarpenter2 Nov 28 '17 at 9:59
  • $\begingroup$ Your link format is wrong. It should be like this: link to the paper $\endgroup$ – ice1000 Nov 29 '17 at 13:21
4
$\begingroup$

So, it's possible, but there are certainly some barriers:

  • What kinds of expressions are allowed in types? What does it mean for a type to have a side-effect? Can typrchecking my program perform IO?
  • Just because dependent types are in the system doesn't mean they provide a type safe language. It may be possible to produce proofs of False if the underlying type system is not consistent.
  • Many imperative languages don't have type systems complex enough to make dependent types useful. For example, Go has no higher kinded types, so if you can't index types by types, indexing types by values probably won't work.
  • Depending on the language, some additional type annotations might be necessary to make type checking decidable.
  • It may be hard to interpret dependent types in the context of side effects. What does a value of type $x=y$ even mean if $x,y$ can change their values at runtime? Does this mean a term can be well typed at one point, and dynamically become ill typed? Or can you only use dependent types for immutable values?

I'm sure that imperative dependent types are possible. In particular, I'd keep my eyes on Rust for adding these in a limited way.

But doing dependent types in a pure functional language is just so much easier.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.