Andy Melnikov (nponeccop) wrote,
Andy Melnikov
nponeccop

Выходные, время изобретать всякую ерунду. Вот смотрите, что я изобрел. Мне кажется, очень компактно иллюстрируется куча вещей. А теоремы какие разнообразные получаются! Интересно, занимался ли кто-то развитием этого направления (голый rank 1 fragment of system F + явные proof terms), и можно ли из этого сделать что-то практически пригодное?

data Add a b
data Sub a b
data GTE a b

geqRefl :: GTE a a
geqRefl = undefined

geqAdd :: GTE (Add a b) b
geqAdd = undefined

addComm :: GTE (Add a b) (Add b a)
addComm = undefined

geqTrans :: GTE a b -> GTE b c -> GTE a c
geqTrans = undefined

data Z a = Z { unZ :: Int }

app2 x (Z a) (Z b) = Z $ x a b
app3 x _ (Z a) (Z b) = Z $ x a b

add :: Z a -> Z b -> Z (Add a b)
add = app2 (+)

sub :: GTE a b -> Z a -> Z b -> Z (Sub a b)
sub = app3 (-)

a1 a b = add a b
a2 = add (Z 5) (Z 6)
a3 = sub geqAdd (add (Z 5) a) a where a = Z 0
a4 = sub geqRefl a a where a = Z 0
a5 a b c = sub p1 (add (add a b) c) a
p1 = geqTrans (geqTrans addComm geqAdd) (geqTrans addComm geqAdd)
a6 = a5 (Z 0) (Z 0) (Z 0)
Вопрос студии: почему p1 нельзя сократить до let x = ... in geqTrans x x?
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 11 comments