Anyone using related techniques or interested in using them? Personally I found my way through with trial and error - it would be cool to hear other's experiences with encoding runtime information in types.
I really want to hear if anyone had an easy time learning dependent types in Haskell. From my experience it was a nightmare figuring out what language extensions I wanted when doing X, and all of the weird edge cases of the syntax. Nowadays when I want to play around with dependent types I always reach for Idris and not Haskell because in my opinion it is so much more straight forward.
Anyone using related techniques or interested in using them? Personally I found my way through with trial and error - it would be cool to hear other's experiences with encoding runtime information in types.
I really want to hear if anyone had an easy time learning dependent types in Haskell. From my experience it was a nightmare figuring out what language extensions I wanted when doing X, and all of the weird edge cases of the syntax. Nowadays when I want to play around with dependent types I always reach for Idris and not Haskell because in my opinion it is so much more straight forward.
@TheMatten You mean
dependent-sum
,aeson-gadt-th
, family of libraries?In general - e.g. playing with existentials
Or emulating sigma type