Есть ли функция для извлечения значения из Singleton?

Question

Я разрабатываю тип данных, который требует SNat, и хотел бы иметь возможность дать пользователю Nat вместо этого. Поиск в Google еще не дал результатов.

То есть есть функция

f :: forall a (x :: a). Sing a x -> a

Answer 1

Вы можете использовать fromSing из singletons