Program extraction for dependently-typed languages such as Rocq often requires unsafe type casts. In this work in progress I introduce Extractly, a first-order language with data types and codata types inspired by Binder et. al.’s Polarity. Restrictions on large elimination help remove the dependence of types on terms, whilst changes to well-formedness checking of data types ensure little-to-no loss in expressivity.