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.