This part of the tutorial explains Pi-types basically. There is a basic example of Pi type \Pi (b : Bool) -> if b Nat Bool. Most of the examples in the section with Basics are supported by their counterparts in Haskell. I would give a Haskell counterpart of \Pi (b : Bool) -> if b Nat Bool as well to emphasise how dependently typed languages relief dealing with type-level stuff. It could be of help (for a Haskell part of the potential audience) in making a difference between Haskell and Arend stressing that dependent types in Arend are proper.
\Pi (b : Bool) -> if b Nat Bool could be translated via type families and the language extension call DataKinds.
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
import Data.Kind (Type)
type family Foo (b :: Bool) :: Type where
Foo 'True = Nat
Foo 'False = Bool
This part of the tutorial explains Pi-types basically. There is a basic example of Pi type
\Pi (b : Bool) -> if b Nat Bool. Most of the examples in the section with Basics are supported by their counterparts in Haskell. I would give a Haskell counterpart of\Pi (b : Bool) -> if b Nat Boolas well to emphasise how dependently typed languages relief dealing with type-level stuff. It could be of help (for a Haskell part of the potential audience) in making a difference between Haskell and Arend stressing that dependent types in Arend are proper.\Pi (b : Bool) -> if b Nat Boolcould be translated via type families and the language extension callDataKinds.