Skip to content

Instantly share code, notes, and snippets.

@hgiasac

hgiasac/typeable27.hs Secret

Created January 4, 2019 17:55
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 hgiasac/04d042773d726353b0258c1a4a38bcc7 to your computer and use it in GitHub Desktop.
Save hgiasac/04d042773d726353b0258c1a4a38bcc7 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
typeable27.hs
dynFst :: Dynamic -> Maybe Dynamic
-- dynFst (Dyn (rpab :: TypeRep pab) (x :: pab))
dynFst (Dyn (TrApp _ (rpa :: TypeRep pa) (rb :: TypeRep b)) (x :: pab))
-- introduces kind k2, and types pa :: k2 -> *; b :: k2
= case rpa of
TrApp (rp :: TypeRep p) (ra :: TypeRep a) ->
-- introduces kind k1, and types p :: k1 -> k2 -> *, a :: k1
case eqT rp (typeRep :: TypeRep (,)) of
Just Refl -> Just $ Dyn ra (fst x)
-- introduces p ~ (,) and (k1 -> k2 -> *) ~ (* -> * -> *)
Nothing -> Nothing
_ -> Nothing
dynFst _ = Nothing
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment