8
$\begingroup$

Is it possible to use Dependent Types in the existing Typed Racket implementation? (ie do they exist in it?)

Is it reasonably possible to implement a Dependent Types System using Typed Racket?

$\endgroup$
  • 3
    $\begingroup$ I think you need to clarify this question a bit: are you asking whether dependent types exist in Racket or weather it is possible to add them? If it's the former, then no (by most reasonable definitions of dependent types), and if it's the latter, then yes. $\endgroup$ – cody Oct 8 '13 at 18:14
  • 1
    $\begingroup$ As cody notes, this question is unclear, and depending on what you meant the answer is either a not-very-interesting no or a not-very-interesting yes. Please flesh out this question so that we know what you are actually asking. $\endgroup$ – Gilles Oct 8 '13 at 19:34
4
$\begingroup$

Dependent Types in Racket are being worked on by Andrew Kent at Indiana University.

There is a set of slides. There is a talk.

Of interest, this potentially also impacts Typed Clojure, which is strongly modelled on Typed Racket.

$\endgroup$
-1
$\begingroup$

I think to "do dependent types" using contracts is already possible. Check https://docs.racket-lang.org/guide/contracts-struct.html and look for "Checking Properties of Data Structures".

You could argue, that this is rather simulating the effect, than having it as part of the language. However, somewhere you'll need to write the code, which tells the interpreter/compiler what those dependencies are and in Racket you can do that with contracts.

$\endgroup$
  • $\begingroup$ I'm happy with the idea that macros in racket are 'extending the compiler' $\endgroup$ – hawkeye Jul 11 '17 at 0:28
  • $\begingroup$ @hawkeye Could you provide an answer to this question implementing dependent types with macros? (I do not doubt it is possible.) $\endgroup$ – Zelphir Kaltstahl Jul 11 '17 at 7:50
  • $\begingroup$ The argument about whether macros extend the compiler are here: stackoverflow.com/a/268091/15441 and you can put any piece of code into a macro - so the code that is used for dependent types can be put into a macro. That was the point I was making. $\endgroup$ – hawkeye Jul 12 '17 at 9:06

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.