Skip to content

Instantly share code, notes, and snippets.

@jrslepak

jrslepak/gist:5099883

Last active December 14, 2015 14:19
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/5099883 to your computer and use it in GitHub Desktop.
Save jrslepak/5099883 to your computer and use it in GitHub Desktop.
Download ZIP
composition operations for testing type checker
Raw
gistfile1.rkt
; typing compose makes use of typechecker code for handling abstracted indices
(check-equal?
(judgment-holds
(type-of [] [] []
(I-λ [(s1 Shape) (s2 Shape) (s3 Shape)]
(T-λ [α β γ]
(A [] [(λ [(f (Array (S) ((Array s1 α) -> (Array s2 β))))
(g (Array (S) ((Array s2 β) -> (Array s3 γ))))]
(A [] [(λ [(x (Array s1 α))] (g (f x)))]))])))
type) type)
(term ((Π [(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 γ))))))))))
; so does typing a fork composition
(check-equal?
(judgment-holds
(type-of
[] [] []
(I-λ [(s-li Shape) (s-lo Shape) (s-ri Shape) (s-ro Shape) (s-jo Shape)]
(T-λ [t-li t-lo t-ri t-ro t-jo]
(A [] [(λ ([f-l (Array (S) ((Array s-li t-li)
-> (Array s-lo t-lo)))]
[f-r (Array (S) ((Array s-ri t-ri)
-> (Array s-ro t-ro)))]
[f-j (Array (S) ((Array s-lo t-lo)
(Array s-ro t-ro)
-> (Array s-jo t-jo)))])
(A [] [(λ [(x (Array s-li t-li))
(y (Array s-ri t-ri))]
(f-j (f-l x) (f-r y)))]))])))
type) type)
(term ((Π ((s-li Shape) (s-lo Shape) (s-ri Shape) (s-ro Shape) (s-jo Shape))
(∀ (t-li t-lo t-ri t-ro t-jo)
(Array (S) ((Array (S) ((Array s-li t-li)
-> (Array s-lo t-lo)))
(Array (S) ((Array s-ri t-ri)
-> (Array s-ro t-ro)))
(Array (S) ((Array s-lo t-lo)
(Array s-ro t-ro)
-> (Array s-jo t-jo)))
-> (Array (S) ((Array s-li t-li)
(Array s-ri t-ri)
-> (Array s-jo t-jo))))))))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment