ICFP 2014: Depending on Types - Stephanie Weirich

no - you run into limitations (eg no GADT promotion, type families need to be saturated, limited unifier doesn't deal with injectivity); you cannot write everything doable in Agda, yet. see the ICFP 2014 keynote linked in the article for an overview of where it's at and where it's going link to this video . also HIW 2014 "Dependent Haskell" talk link to this video , and, for lifting some of the restrictions right now, eg the saturatedness of type functions, the haskell syposium 2014 talk on the new additions to the singletons library link to this video - where they enable promoting functions including unsaturated ones to type level. further work on the matter linked there - https://ghc.haskell.org/trac/ghc/wiki/Depende…

It does a... little. It certainly can do an approximation of dependently typed programming to a level that surprised me, up to one level of type promotion. That being said, I'm an Agda enthusiast and definitely would love fully dependent types in Haskell. Would highly recommend this talk: link to this video