Recursion through delayed evalution impossible?

 So, I want to do something in agda, consider the following type:

data Genlist (A : Set) : Set where
  cons : A -> Genlist A -> Genlist A
  generator : ((tt : ⊤) -> Genlist A) -> Genlist A

The type captures the notion of finite but expandable lists. But because agda doesn't understand that delaying a computation can guarantee termination I need to bypass the type checker with a pragma.

  {-# TERMINATING #-}

  ones : Genlist Nat

  ones = generator (\x -> cons 1 ones)

Unfortunately, that also comes with the following cost. You can prove that the type isn't inhabited.

  data ⊥ : Set where

  uhh : ∀ {A} → Genlist A → ⊥

  uhh (cons _ x)    = uhh x

  uhh (generator x) = uhh (x tt)

The type system needed would, apart from allowing recursion with delayed computation, also need to keep track of how often you force a computation.

Oh, really?

 Okay, we have this in Agda:

module I where

open import Data.Unit
open import Relation.Binary.PropositionalEquality

private variable
A : Set

to : (⊤ → A) → A
to f = f tt

from : A → ⊤ → A
from x _ = x

to∘from : ∀ {A} (x : A) → to (from x) ≡ x
to∘from _ = refl

from∘to : ∀ {A} (x : ⊤ → A) → from (to x) ≡ x
from∘to _ = refl

We can abstract away from computation... This makes sense for a total specification language, all computations terminate with some answer and therefore you can substitute that answer.

But it is a bit suspect, and possibly restrictive, at the same time too.

Edit: It's more than suspect but absurd.

Dabbling with Agda

I am dabbling with Agda since I want to do something. Can you figure out what?

module Kripke where

open import Data.List.Base as List using (List; []; _∷_)

open import Data.List.NonEmpty as List⁺ using (List⁺; [_]; _∷_)

open import Agda.Builtin.Unit using (⊤; tt)

{- I want to study finite semantics for temporal logic formula over automata -}

{- Kripke structures, maybe switch to labeled transition systems -}

record Kripke (S : Set) (AP : Set) : Set where

  field

    initial : List⁺ S

    transition : (s : S) → List⁺ S

    interpretation : (s : S) → List AP

{- a tree could suffice to describe the semantics for an automaton

   but fails to capture the unravelling of an automaton in the type

   itself -}

data Tree (A : Set) : Set where

  leaf : List A -> Tree A

  branch : A -> List (Tree A) → Tree A

{- instead, the 'clever' idea is to use the following structure, any leaf node

   can be unravelled further into a tree with a generating function -}

data GenTree (A : Set) : Set where

  branch : A -> List (GenTree A) → GenTree A

  generator : ((tt : ⊤) -> GenTree A) -> GenTree A

{- so maybe first try it for lists -}

data GenList (A : Set) : Set where

  cons : A -> GenList A -> GenList A

  generator : ((tt : ⊤) -> GenList A) -> GenList A