Skip to content

Instantly share code, notes, and snippets.

@jrslepak

jrslepak/gist:5095779

Last active December 14, 2015 13:48
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save jrslepak/5095779 to your computer and use it in GitHub Desktop.
Save jrslepak/5095779 to your computer and use it in GitHub Desktop.
Download ZIP
typing compose
Raw
gistfile1.txt
> (judgment-holds
(type-of []
[]
[]
(Λ [α β γ]
(A []
[(λ [(f 0 (Array (S) ((Array (S) α) -> (Array (S) β))))
(g 0 (Array (S) ((Array (S) β) -> (Array (S) γ))))]
(A [] [(λ [(x 0 (Array (S) α))] (g (f x)))]))]))
type)
type)
'((∀
(α β γ)
(Array
(S)
((Array (S) ((Array (S) α) -> (Array (S) β)))
(Array (S) ((Array (S) β) -> (Array (S) γ)))
->
(Array (S) ((Array (S) α) -> (Array (S) γ)))))))
> (judgment-holds
(type-of []
[]
[]
(ל [(s1 Shape) (s2 Shape) (s3 Shape)]
(Λ [α β γ]
(A []
[(λ [(f 0 (Array (S) ((Array s1 α) -> (Array s2 β))))
(g 0 (Array (S) ((Array s2 β) -> (Array s3 γ))))]
(A [] [(λ [(x 0 (Array s1 α))] (g (f x)))]))])))
type)
type)
'((Π
((s1 Shape) (s2 Shape) (s3 Shape))
(∀
(α β γ)
(Array
(S)
((Array (S) ((Array s1 α) -> (Array s2 β)))
(Array (S) ((Array s2 β) -> (Array s3 γ)))
->
(Array (S) ((Array s1 α) -> (Array s3 γ))))))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment