Dependent Types


#1

I’m interested in getting ahead of the curve on learning Plutus, IELE, and other Cardano/IOHK tech for use in my future DApps. Does anyone know if Plutus uses dependent types like Idris or do they need to be extended w/ singletons like in Haskell? I think that’s one of the bigger features that Haskell misses out on in comparison to Idris. Of course, it can be done by using singletons and is being proposed for a future version of GHC, but it is currently a feature that would be useful for dev.

My most enthusiastic bit of advice to IOHK and Cardano Foundation is to start compiling tutorials for future devs. I know it’s way too early but I hope they have tutorials at release.


#2

Unfortunately I can’t answer your question I guess extensive Plutus spec docs contains it.


#3

It’s not in the Plutus spec docs unless it’s hidden in some equation that I can’t decipher.


#4

Would be an option putting the question in an issue in the aforementioned repository?