granule. A statically-typed linear functional language with graded modal types for fine-grained program reasoning