{-# LANGUAGE Safe #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE GADTs, KindSignatures, ScopedTypeVariables #-}
module Copilot.Core.Type.Dynamic
( Dynamic (..)
, DynamicF (..)
, toDyn
, fromDyn
, toDynF
, fromDynF
) where
import Copilot.Core.Type.Equality
data Dynamic :: (* -> *) -> * where
Dynamic :: a -> t a -> Dynamic t
data DynamicF :: (* -> *) -> (* -> *) -> * where
DynamicF :: f a -> t a -> DynamicF f t
toDyn :: t a -> a -> Dynamic t
toDyn :: t a -> a -> Dynamic t
toDyn t a
t a
x = a -> t a -> Dynamic t
forall a (t :: * -> *). a -> t a -> Dynamic t
Dynamic a
x t a
t
fromDyn :: EqualType t => t a -> Dynamic t -> Maybe a
fromDyn :: t a -> Dynamic t -> Maybe a
fromDyn t a
t1 (Dynamic a
x t a
t2) =
case t a
t1 t a -> t a -> Maybe (Equal a a)
forall (t :: * -> *) a b.
EqualType t =>
t a -> t b -> Maybe (Equal a b)
=~= t a
t2 of
Just Equal a a
Refl -> a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
Maybe (Equal a a)
Nothing -> Maybe a
forall a. Maybe a
Nothing
toDynF :: t a -> f a -> DynamicF f t
toDynF :: t a -> f a -> DynamicF f t
toDynF t a
t f a
fx = f a -> t a -> DynamicF f t
forall (f :: * -> *) a (t :: * -> *). f a -> t a -> DynamicF f t
DynamicF f a
fx t a
t
fromDynF :: EqualType t => t a -> DynamicF f t -> Maybe (f a)
fromDynF :: t a -> DynamicF f t -> Maybe (f a)
fromDynF t a
t1 (DynamicF f a
fx t a
t2) =
case t a
t1 t a -> t a -> Maybe (Equal a a)
forall (t :: * -> *) a b.
EqualType t =>
t a -> t b -> Maybe (Equal a b)
=~= t a
t2 of
Just Equal a a
Refl -> f a -> Maybe (f a)
forall (m :: * -> *) a. Monad m => a -> m a
return f a
fx
Maybe (Equal a a)
Nothing -> Maybe (f a)
forall a. Maybe a
Nothing