transcribe.idr

module Main

namespace DNA
  data Nucleotide : Char -> Type where
    A : Nucleotide 'A'
    C : Nucleotide 'C'
    G : Nucleotide 'G'
    T : Nucleotide 'T'

namespace RNA
  data Nucleotide : Char -> Type where
    A : Nucleotide 'A'
    C : Nucleotide 'C'
    G : Nucleotide 'G'
    U : Nucleotide 'U'

data Every : (a -> Type) -> List a -> Type where
      Nil  : { P : a -> Type }                      -> Every P []
      (::) : { P : a -> Type } -> P x -> Every P xs -> Every P (x :: xs)

transcribe : (s : String) -> { p : Every Dna.Nucleotide dna } -> Every Rna.Nucleotide rna
transcribe = ?transcribe_rhs

transcribe.scala

sealed trait Nucleotide

object Nucleotide {
  sealed trait DNA extends Nucleotide
  sealed trait RNA extends Nucleotide

  object A extends Nucleotide with DNA with RNA
  object C extends Nucleotide with DNA with RNA
  object G extends Nucleotide with DNA with RNA
  object T extends Nucleotide with DNA
  object U extends Nucleotide          with RNA
}

import Nucleotide.{A, C, G, T, U}

type DNA = Seq[Nucleotide.DNA]
type RNA = Seq[Nucleotide.RNA]

def transcribe(dna: DNA): RNA = dna map {
  // using cast
  // case T => U
  // case n => n.asInstanceOf[Nucleotide.RNA]
  // or explicitly
  case A => A
  case C => C
  case G => G
  case T => U
}


val dna: DNA = Seq(A, C, G, T) // won't compile if add U => Seq(A, C, G, U)
val rna: RNA = Seq(A, C, G, U) // won't compile if add T => Seq(A, C, G, T)
val nucleotides: Seq[Nucleotide] = dna ++ rna

transcribe(dna) == rna

transribe.hs

-- Three files in one
-- Main.hs
module Main where

import qualified DNA as DNA
import           DNA   (DNA)
import qualified RNA as RNA
import           RNA   (RNA)

main :: IO ()
main = interact (show . transcribe . read)

transcribe :: DNA -> RNA
transcribe = map toRna where
  toRna DNA.A = RNA.A
  toRna DNA.C = RNA.C
  toRna DNA.G = RNA.G
  toRna DNA.T = RNA.U

-- DNA.hs
module DNA where

import qualified Text.Read                     as R
import qualified Text.Read.Lex                 as L
import qualified Text.ParserCombinators.ReadP  as P

import Text.Read ((<++))

data Nucleotide = A | C | G | T deriving (Eq)

type DNA = [Nucleotide]

instance Show Nucleotide where
  show A = "A"
  show C = "C"
  show G = "G"
  show T = "T"

  showList = flip (foldr ((++) . show))

instance Read Nucleotide where
  readPrec = R.parens (R.lift parseNucleotide)
  
  readListPrec = R.readListPrecDefault <++ R.parens (R.lift (P.many parseNucleotide))

parseNucleotide :: P.ReadP Nucleotide
parseNucleotide = P.choice [ P.char 'A' >> return A
                           , P.char 'C' >> return C
                           , P.char 'G' >> return G
                           , P.char 'T' >> return T
                           ]

-- RNA.hs
module RNA where

import qualified Text.Read                     as R
import qualified Text.Read.Lex                 as L
import qualified Text.ParserCombinators.ReadP  as P

import Text.Read ((<++))

data Nucleotide = A | C | G | U deriving (Eq)

type RNA = [Nucleotide]

instance Show Nucleotide where
  show A = "A"
  show C = "C"
  show G = "G"
  show U = "U"

  showList = flip (foldr ((++) . show))

instance Read Nucleotide where
  readPrec = R.parens (R.lift parseNucleotide)
  
  readListPrec = R.readListPrecDefault <++ R.parens (R.lift (P.many parseNucleotide))

parseNucleotide :: P.ReadP Nucleotide
parseNucleotide = P.choice [ P.char 'A' >> return A
                           , P.char 'C' >> return C
                           , P.char 'G' >> return G
                           , P.char 'U' >> return U
                           ]