Draugatög @ RFP 2020-06-25

README.md

Sæktu https://github.com/tritlo/writ-plugin, búðu til nýja möppu sem heitir TestRFP, bættu því við í cabal.project og afritaðu skjölin hér að ofan í möppuna, og keyrðu svocabal run test_rfp til að keyra

Test.hs

{-# OPTIONS_GHC -fplugin=WRIT.Plugin
                -fplugin-opt=WRIT.Plugin:debug
 #-}
module Main where

import GHC.TypeLits
import WRIT.Configure

data Lengd = Amk Nat | Óþekkt

newtype Vigur (l :: Lengd) a = Vigur [a] deriving (Show)

(>:) :: a -> Vigur l a -> Vigur (Viðbætt l) a
a >: (Vigur xs) = Vigur (a:xs)

type family Viðbætt (l :: Lengd) :: Lengd where
    Viðbætt Óþekkt = Amk 1
    Viðbætt (Amk n) = Amk (n+1)

höfuð :: (1 <= n) => Vigur (Amk n) a -> a
höfuð (Vigur (a:_)) = a


type family TekiðAf (l :: Lengd) :: Lengd where
    TekiðAf Óþekkt = Óþekkt
    TekiðAf (Amk 0) = Óþekkt
    TekiðAf (Amk n) = Amk (n-1)

hali :: Vigur lengd a -> Vigur (TekiðAf lengd) a
hali (Vigur (_:xs)) = Vigur xs

hal :: forall a lengd . Vigur lengd a -> Vigur Óþekkt a
hal = tail @a

öruggurhali :: (lengd ~ Amk n, 1 <= n) => Vigur lengd a -> Vigur (TekiðAf lengd) a
öruggurhali (Vigur (_:xs)) = Vigur xs

úrLista :: [a] -> Vigur Óþekkt a
úrLista = Vigur

vigurinnMinn :: Vigur (Amk 2) Bool
vigurinnMinn = Vigur [True]

type instance Promote [a] (Vigur Óþekkt a) =
    Msg (Text "Breytti lista í vigur")

type instance Promote (Vigur _ a) [a] =
    Msg (Text "Breytti vigri í lista")

type instance Default Lengd = Óþekkt

hinnVigurinnMinn :: Vigur (Amk 1) Bool
hinnVigurinnMinn = Vigur [True]

main :: IO ()
main = do let v = úrLista [True, False, False]
              v2 = True>:v
          print (höfuð v2)
          print (höfuð $ hali vigurinnMinn)
          print (öruggurhali $ öruggurhali hinnVigurinnMinn)

TestRFP.cabal

name: TestRFP
cabal-version: >= 1.24
build-type: Simple
version: 1.0.0

executable test_rfp
  default-language: Haskell2010
  build-depends:  base >= 4 && < 5,
                  writ-plugin <= 1
  extensions: DataKinds,
              FlexibleInstances,
              MultiParamTypeClasses,
              FlexibleContexts,
              TypeFamilies,
              PolyKinds,
              UndecidableInstances,
              TypeOperators,
              TypeApplications,
              ScopedTypeVariables,
              RoleAnnotations
  main-is: Test.hs