Hey all,

I published an article a week-ish ago about dependent and impredictive types, and there is one code example in it that I still don’t quite understand. I’d love to harness it somehow & make a library out of it for working with impredictive types in PureScript, but first I’d like to understand what’s going on & could use some help.

Here’s the JS FFI for the example:

```
// Main.js for the foreign import
exports.arr0 = function () {
return [1, 2, 3, 4, 5];
};
```

And here is the PS:

```
module Test.Main where
import Prelude
import Control.Monad.Indexed (class IxApplicative, class IxApply, class IxBind, class IxFunctor, class IxMonad)
import Control.Monad.Indexed.Qualified as Ix
import Data.List (List(..), fromFoldable)
import Data.Newtype (class Newtype, unwrap)
import Effect (Effect)
import Effect.Class (class MonadEffect)
import Effect.Class.Console (log)
import Type.Proxy (Proxy(..))
data Unk
foreign import data Unk0 :: Unk
foreign import data UnkX :: Unk -> Unk
newtype MUnk (i :: Unk) (o :: Unk) a
= MUnk (Effect a)
derive instance newtypeUnk :: Newtype (MUnk i o a) _
derive newtype instance functorMUnk :: Functor (MUnk i o)
derive newtype instance applicativeMUnk :: Applicative (MUnk i o)
derive newtype instance applyMUnk :: Apply (MUnk i o)
derive newtype instance bindMUnk :: Bind (MUnk i o)
derive newtype instance monadMUnk :: Monad (MUnk i o)
derive newtype instance monadEffectMUnk :: MonadEffect (MUnk i o)
instance munkIxFunctor :: IxFunctor MUnk where
imap f (MUnk a) = MUnk (f <$> a)
instance munkIxApplicative :: IxApply MUnk where
iapply (MUnk f) (MUnk a) = MUnk (f <*> a)
instance munkIxApply :: IxApplicative MUnk where
ipure a = MUnk $ pure a
instance munkIxBind :: IxBind MUnk where
ibind (MUnk monad) function = MUnk (monad >>= (unwrap <<< function))
instance munkIxMonad :: IxMonad MUnk
class TLShow :: ∀ (k ∷ Type). k → Constraint
class TLShow i where
tlShow :: Proxy i -> String
instance tlShowUnk0 :: TLShow Unk0 where
tlShow _ = "Unk0"
instance tlShowUnkX :: TLShow x => TLShow (UnkX x) where
tlShow _ = "UnkX (" <> tlShow (Proxy :: Proxy x) <> ")"
class IxRec m where
next :: forall (i :: Unk) a. Show a => TLShow i => a -> m i (UnkX i) a
done :: forall (i :: Unk). m i Unk0 Unit
iFor_ :: forall (i :: Unk) m a. Show a => TLShow i => IxRec m => IxMonad m => List a -> m i Unk0 Unit
iFor_ Nil = done
iFor_ (Cons a b) = Ix.do
_ <- next a
iFor_ b
printMUnk :: forall (i :: Unk). TLShow i => MUnk i i Unit
printMUnk = Ix.do
log $ tlShow (Proxy :: Proxy i)
instance ixRec :: IxRec MUnk where
next a = Ix.do
printMUnk
log $ show a
pure a
done = pure unit
foreign import arr0 :: Effect (Array Int)
main :: Effect Unit
main = do
list0 <- fromFoldable <$> arr0
let (MUnk o) = (iFor_ :: List Int -> MUnk Unk0 Unk0 Unit) list0
o
```

Resulting in the output

```
Unk0
1
UnkX (Unk0)
2
UnkX (UnkX (Unk0))
3
UnkX (UnkX (UnkX (Unk0)))
4
UnkX (UnkX (UnkX (UnkX (Unk0))))
5
```

What still blows my mind here is that the `Unk`

-s can be constructed inductively counting up even though we do not know what the actual type will be at compile time. Previously, I had only ever used recursively defined types (ie printing typelevel peanos) using completely determined types, meaning something like `show (Proxy :: Proxy (Succ Z))`

. Here, even though an indexed type `i`

with type `UnkX (UnkX (UnkX (UnkX (Unk0))))`

“exists” in the program, it is nowhere specifically written out, nor can its existence be worked out deductively by following recursive functions backwards. Its existence is completely determined by an unknown array in the FFI.

Are there any other examples of this in the PureScript ecosystem? I think if I could find more examples, I could get more comfortable with the concept of a “type that is unknown and cannot be known by the compiler at compile time” (if that’s what you can call it), but I’m coming up short.

My goal is to build out a general library for control structures for indexed monads where the control operator does some sort of incrementing of the index (ie `ixFor_`

in the example above, etc) but first it’d be good to actually understand what’s going on here.

Thanks for your ideas/help!

~Mike