A revolutionary framework explaining why AlphaFold works. Anfinsen's dogma is type safety. Deep learning succeeds because protein folding is a well-typed problem.
-- Protein folding as type inference
data Structure (s :: Sequence) where
-- Structure depends on sequence
fold :: (s :: Sequence) -> Maybe (Structure s)
fold s = proofSearch (constraints s)
-- Anfinsen's Dogma (Type Safety):
-- For type-safe sequences,
-- |Structure(s)| = 1 ✓AlphaFold's success isn't just "we threw enough compute at it"—it's that protein folding has the right structure for learning to work.
Anfinsen's dogma guarantees sequences uniquely determine structures—exactly like well-typed programs have unique normal forms.
AlphaFold doesn't discover physics—it learns efficient proof search heuristics within a constraint space defined by thermodynamics.
Multiple Sequence Alignments provide type annotations that narrow the search space. Co-evolution reveals dependent constraints.
The framework predicts AlphaFold's failures: IDPs (type underdetermined), prions (non-confluent), shallow MSAs (insufficient annotations).
| Protein Folding | Type Theory |
|---|---|
| Amino acid sequence | Type signature |
| Native 3D structure | Canonical term / normal form |
| Folding process | Term normalization / proof search |
| Thermodynamic constraints | Typing rules |
| Energy minimum | Normal form |
| Chaperone proteins | Type checker / proof assistant |
| MSA (evolutionary data) | Type annotations / hints |
| Triangle inequality | Refinement type |
Master type-safe biophysics from foundations to applications.
The Haskell implementation demonstrates type safety in biophysics.
-- Amino acid sequence is the TYPE SIGNATURE
type Sequence = [AminoAcid]
-- Structure DEPENDS on sequence
data Structure (s :: Sequence) where
MkStructure :: Coordinates
-> ConstraintsSatisfied s
-> Structure s
-- The fold function: proof search
fold :: (s :: Sequence) -> Maybe (Structure s)
fold s = search (constraints s)-- For type-safe sequences:
-- |Structure(s)| = 1
data AnfinsenProof where
AnfinsenPrf
:: Sequence -- The type
-> Structure -- Unique inhabitant
-> UniqueMinimum -- Proof of uniqueness
-> KineticAccessible -- Reachable
-> AnfinsenProof-- AlphaFold learns HEURISTICS,
-- not physics
runAlphaFold :: Sequence -> MSA -> Structure
runAlphaFold seq msa =
let -- MSA provides type annotations
typeHints = extractConstraints msa
-- Evoformer propagates constraints
refined = evoformer typeHints
-- Structure module constructs proof
in constructProof refinedgit clone https://github.com/MagnetonIO/type-safe-biophysics
cd type-safe-biophysics/haskell
stack build && stack exec type-safe-biophysics-exeUse these prompts with Claude or GPT to deepen your understanding.
Deep dive into the core framework
AlphaFold as learned proof search
Framework's predictive power
Hands-on implementation
Beyond protein folding
Broader ML theory
We propose a novel theoretical framework for understanding AlphaFold's success. Protein folding is fundamentally type-safe: Anfinsen's thermodynamic hypothesis guarantees that amino acid sequences deterministically map to native structures, analogous to how well-typed programs have unique normal forms. AlphaFold learns efficient proof search heuristics, not protein physics.
Download PDF"Machine learning systems don't need to discover the laws of physics. They need to learn efficient navigation of constraint spaces that physics has already defined."
"AlphaFold is not discovering protein chemistry. It's learning proof search heuristics within a space where thermodynamics guarantees a unique solution exists."
"The type checker is death. Evolution operates as a dynamically typed language with the most brutal runtime type checker imaginable."
"Type safety may be the fundamental axis for predicting machine learning tractability across domains."