[Haskell-cafe] Runtime selection on types while capturing a dictionary?
Benjamin Redelings
benjamin.redelings at gmail.com
Mon Oct 7 21:38:30 UTC 2024
Hi,
I'm new to Haskell, and I'm writing a class for evolutionary trees.
Since I'm new to Haskell, trying to encode information at the type level
is new to me. In C++ I'd use runtime checks to ask whether (for
example) a tree is rooted. Or I'd have the getRoot function return
Maybe NodeID and then make the methods for checking if a branch points
rootward throw an exception if the tree is unrooted.
I'm trying to avoid doing this the C++ way, but this raises a lot of
question. Let me start with 2 of them:
1. Is there any advice on how to represent data structures that may or
may not have a list of attributes?
But what I have in Haskell right now looks like this:
data Graph (IntMap Node) (IntMap Edge)
data WithBranchLengths t = WithBranchLengths t (IntMap Double)
data WithLabels t l = WithLabels t (IntMap (Maybe l))
data Forest = Forest Graph {- Assert that the Graph is a Forest -}
data WithRoots t = WithRoots t [NodeId]
data WithNodeTimes t = WithNodeTimes t (IntMap Double)
data WithBranchRates t = WithBranchRates t (IntMap Double)
data Tree = Tree Forest {- Assert that the Forest is a
Tree -}
A tree with labels, roots, and branch lengths could have following types:
WithLabels (WithRoots (WithBranchLengths Tree)) Text
WithLabels (WithBranchLengths (WithRoots Tree)) Text
WithRoots (WithLabels (WithBranchLengths Tree) Text)
WithRoots (WithBranchLengths (WithLabels Tree Text))
.. etc etc..
The fact that there are multiple ways to represent the same thing is
already not great. 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. Only the outer
WithBranchLengths is going to count, and there really should not be two
of the same attribute.
2. I'm wondering if it is possible to do run-time selection on whether
a tree is rooted or not. (I've considered trying to move all checks to
the type-level, but this inhibits putting models with different
properties into the same list -- see below)
class IsGraph g where
...
class IsGraph g => IsDirectedGraph g where
isForward :: g -> EdgeId -> Bool
class IsDirectedGraph g => IsDirectedAcyclicGraph g
class IsGraph f => IsForest f where
type family Unrooted f
type family Rooted f
unroot :: f -> Unrooted f
makeRooted :: f -> Rooted f
class (IsDirectedAcyclicGraph t, IsForest t) => HasRoots t where
isRoot :: t -> NodeId -> Bool
roots :: t -> [NodeId]
isRoot f n = isSource f n
roots f = filter (isRoot f) (getNodes f)
At first I was thinking that since rooting is at the type level, then I
can't do any runtime branching on whether a tree is rooted. But then it
occured to me that a GADT can package dictionaries with a constructor,
so that in theory I could do something like:
likelihood s t = if isEquilibriumReversible s then
equilibriumReversibleLikelihood s t
else case isRooted t of Unrooted -> error "tree must
be rooted, since model is not reversible or not at equilibrium!"
Rooted ->
rootedTreeLikelihood s t
It seems like this might work if I could make a GADT with a signature
something like:
data MaybeRooted t = Unrooted | HasRoots t => Rooted
-- Q: should this use a forall type?
In that case the Rooted constructor would package the HasRoots t
dictionary needed to run the rootedTreeLikelihood function. But I'm not
sure how I would actually write the `isRooted` function that would
construct the MaybeRooted t data type. I've considered trying to encode
the EquilibriumReversible predicate at the type level to avoid runtime
checks, but that has the problem that I couldn't put models with
different properties into the the same list of type [m].
So I guess the questions are:
Q2a: is this a reasonable way of trying to do runtime selection on
whether a tree is rooted?
Q2b: how would I write the `isRooted t` function?
Feedback much appreciated.
-BenRI
P.S. Haskell code is here:
https://github.com/bredelings/BAli-Phy/tree/master/haskell
More information about the Haskell-Cafe
mailing list