В idris есть вселенная под названием UniqueType значения типов, в которых можно использовать только один раз. Насколько мне известно, его можно использовать для написания высокопроизводительного кода.
Как это сделать в чистом виде? псевдокод: loop:
input = read_stdin
if input == "q":
break loop
else:
print "you input: ", input
На самом деле, я имел взгляд на каком-то PD