Where do i start if i want to play with dependent types in Haskell?
I use final tagless encoding in Haskell for DSLs that compile to C / Verilog and I got lost in Haskell's language extension zoo trying to do more type level encoding
Should I jump to Idris instead?
Conversation
Maybe I misunderstood and there is no clear cut way to do dependent types (yet?), only a couple of different ad-hoc ways to simulate DT using combinations of extensions?
1
Prob best to play with Idris first...
I think this is pretty much what I'm looking for:
docs.idris-lang.org/en/latest/tuto
1
1
references from Haskell IRC:
How to emulate:
hackage.haskell.org/package/single
Partially implemented plan to integrate in Haskell:
cis.upenn.edu/~sweirich/pape
Replying to
Looking at this it seems a better way to learn Haskell's extension zoo is to learn a DT language first to see the reason for all the type-level extensions. Not sure if this is something I'm just now ready for, or if I stumbled in through the wrong door in the past...