Haskell-Cafe

Download

haskell-cafe@haskell.org

October 2024

22 participants
21 discussions

Re: [Haskell-cafe] Runtime selection on types while capturing a dictionary?
by Olaf Klinke 08 Oct '24

08 Oct '24

> It seems like this might work if I could make a GADT with a signature > something like: > > data MaybeRooted t = Unrooted | HasRoots t => Rooted Yes, that is what GADTs can do for you. But as Tom said, avoid this if cou can. Incidentally, there is a pattern known as "trees that grow" [1] Where a skeleton type has rank-1 parameters that can switch on and off certain constructors. E.g. for a rooted tree you would provide an Identity parameter, for an unrooted tree provide a Const Void or Const () parameter. Small example: data Tree' root branch = Tree' (root [branch (Tree root branch)]) type UnrootedLabeled a = Tree' Identity ((,) a) type RootedLabeled r b = Tree' ((,) r) ((,) b) -- etc. As you observed, this can become confusing, if there are too many variants and the types you actually work with are just type aliases. The advantage is (a) no type classes, (b) you can have pattern-matching functions for a variety of different trees if they do not depend on patterns in the type parameters. > Also, the fact that you can do WithBranchLengths > (WithBranchLengths Tree) indicates that the construction of types > should > be obeying certain rules that are not expressed. Having several type parameters instead of the single t, where every parameter plays a single role, can aid in making rules clearer, but only a GADT may enforce them. There are other rules that only a dependently-typed language will be able to express. Finally, have you tried using one of the existing Haskell graph libraries as a starting point? It may save you a lot of boilerplate code. Olaf [1] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/11/trees-t…

1 0