We study algebraic computational effects and their handlers in the dependently typed setting. We describe computational effects using a generalisation of Plotkin and Pretnar’s effect theories, whose dependently typed operations allow us to capture precise notions of computation, e.g., state with location-dependent store types and dependently typed update monads. Our treatment of handlers is based on an observation that their conventional term-level definition leads to unsound program equivalences being derivable in languages that include a notion of homomorphism. We solve this problem by giving handlers a novel type-based treatment via a new computation type, the user-defined algebra type, which pairs a value type (the carrier) with a family of value terms (the operations), capturing Plotkin and Pretnar’s insight that handlers denote algebras. We show that the conventional presentation of handlers can then be routinely derived. We also demonstrate that this type-based treatment of handlers provides a useful mechanism for reasoning about effectful computations.