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), based on Plotkin and Pretnar’s insight that handlers denote algebras for a given algebraic theory. The conventional presentation of handlers can then be routinely derived from our type-based treatment. We also demonstrate that our treatment of handlers provides a useful mechanism for reasoning about effectful computations.