[Agda] heterogeneous lists with universes

[Andres Loeh]

Hi Jim.

I'm not quite sure what you really want to accomplish.
I've attached three versions of your code that typecheck.
The first is the simplest and doesn't need universes at
all. The second is probably closest to your code, and the
third is the one which I think is closest to being useful.

HTH,
  Andres

-- 

Andres Loeh, Universiteit Utrecht

mailto:andres at cs.uu.nl     mailto:mail at andres-loeh.de
http://www.andres-loeh.de
-------------- next part --------------
module HList where

open import Data.Char

module Version1 where

  data L : (c : Char) -> Set where
    MkL : (c : Char) -> L c 

  infixr 5 _:::_ _::_

  data TCons : Set1 where
    Nil : TCons
    _:::_ : (t : Set) -> TCons -> TCons

  data TSet : TCons -> Set1 where
    []   : TSet Nil
    _::_ : forall {ts A} -> A -> TSet ts -> TSet (A ::: ts)

  example : TSet (L 'A' ::: L 'B' ::: Nil)
  example = MkL 'A' :: MkL 'B' :: []

module Version2 where

  data L : (c : Char) -> Set where
    MkL : (c : Char) -> L c 

  {- I'll add to the types in U later -}
  data U : Set where
    label    : Char -> U

  el : U -> Set
  el (label c) = L c

  infixr 5 _:::_ _::_

  data TCons : Set1 where
    Nil : TCons
    _:::_ : (t : Set) -> TCons -> TCons

  data TSet : TCons -> Set1 where
    []   : TSet Nil
    _::_ : forall {ts u} -> el u -> TSet ts -> TSet (el u ::: ts)

  example : TSet (L 'A' ::: L 'B' ::: Nil)
  example = MkL 'A' :: MkL 'B' :: []

module Version3 where

  data L : (c : Char) -> Set where
    MkL : (c : Char) -> L c 

  {- I'll add to the types in U later -}
  data U : Set where
    label    : Char -> U

  el : U -> Set
  el (label c) = L c

  infixr 5 _::_

  -- normal list
  data List (A : Set) : Set where
    []   : List A
    _::_ : A -> List A -> List A

  data TSet : List U -> Set where
    []   : TSet []
    _::_ : forall {ts u} -> el u -> TSet ts -> TSet (u :: ts)

  example : TSet (label 'A' :: label 'B' :: [])
  example = MkL 'A' :: MkL 'B' :: []