9
$\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$
2
  • 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
    Commented Oct 8, 2013 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$ Commented Oct 8, 2013 at 19:34

2 Answers 2

5
$\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 modeled on Typed Racket.

$\endgroup$
1
-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$
3
  • $\begingroup$ I'm happy with the idea that macros in racket are 'extending the compiler' $\endgroup$
    – hawkeye
    Commented Jul 11, 2017 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$ Commented Jul 11, 2017 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
    Commented Jul 12, 2017 at 9:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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