Skip to content
Hallway
0:00 / 0:00

#haskell#typefamilies#dependenttypes

Haskell 2014: Promoting Functions to Type Families in Haskell, Jan Stolarek

Malcolm Wallace

884 subscribers • 15 videos on Hallway

YouTube
  • Recommended by 2 people: 1 on Lobsters and 1 in engineering communities.
  • Presented by Jan Stolarek

Advanced. Deep dive for people who know the field.

1.8K views12 years ago2 recommendations

Programming languagesFunctional programmingLanguage design and type systems

Jan Stolarek presents a method for automatically promoting term-level functions to type-level type families in Haskell.

Haskell Symposium @ ICFP 2014. Gothenburg, Sweden.

Why it's here

2 people recommend this

What people say. Shared as a key resource on Haskell type-level programming and GHC type family promotion.

bitemyappon Lobsters • Recommends

Haskell 2014: Promoting Functions to Type Families in Haskell, Jan Stolarek
9View on Lobsters

u/WilliamDhalgrenin r/haskell • Recommends

On “Weight-biased leftist heaps verified in Haskell using dependent types”

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…
7View on Reddit