0 | module Data.Container.Base.Concrete.Definition
 1 |
 2 | import Data.Container.Base.Object.Definition
 3 | import Data.Container.Base.Extension.Definition
 4 |
 5 | -- todo rename to `IsConcrete?
 6 | ||| Many Idris' datatypes are already concrete, inductive
 7 | ||| representations of particular containers
 8 | ||| It is useful to be easily able to convert between them
 9 | public export
10 | interface FromConcrete (cont : Cont) where
11 |   constructor MkConcrete
12 |   concreteType : Type -> Type
13 |   concreteFunctor : Functor concreteType
14 |   fromConcreteTy : concreteType a -> Ext cont a
15 |   toConcreteTy : Ext cont a -> concreteType a
16 |   
17 |   
18 | public export
19 | data AllConcrete : List Cont -> Type where
20 |   Nil : AllConcrete []
21 |   Cons : (firstConcrete : FromConcrete c) =>
22 |     (restConcrete : AllConcrete cs) =>
23 |     AllConcrete (c :: cs)
24 |
25 |
26 | -- public export
27 | -- fromConcreteMap : {cont1, cont2 : Cont} ->
28 | --   (fc1 : FromConcrete cont1) => (fc2 : FromConcrete cont2) =>
29 | --   (concreteType @{fc1} a -> concreteType @{fc2} b) ->
30 | --   cont1 `fullOf` a -> cont2 `fullOf` b
31 | -- fromConcreteMap f = fromConcrete @{fc2} . f . toConcrete @{fc1}
32 |