singletons

src/singletons/MySing.lhs

+> {-# LANGUAGE UndecidableInstances #-}
+> {-# LANGUAGE PolyKinds #-}
+> {-# LANGUAGE TemplateHaskell #-}
+> {-# LANGUAGE RankNTypes #-}
+> {-# LANGUAGE FlexibleContexts #-}
+> {-# LANGUAGE FlexibleInstances #-}
+> {-# LANGUAGE KindSignatures #-}
+> {-# LANGUAGE DataKinds #-}
+> {-# LANGUAGE GADTs #-}
+> {-# LANGUAGE TypeOperators #-}
+> {-# LANGUAGE TypeFamilies #-}
+> {-# LANGUAGE TypeApplications #-}
+> {-# LANGUAGE ScopedTypeVariables #-}
+
+> module MySing where
+
+> import Data.Kind
+> import GHC.Exts (Any)
+
+> data Nat = Zero | Succ Nat
+
+> data family Sing (a :: k)
+
+> data instance Sing (a :: Nat) where
+>   SZero :: Sing Zero
+>   SSucc :: (SingRep n) => Sing n -> Sing (Succ n)
+
+
+> type SNat (n :: Nat) = Sing n
+
+--------------------------------------------------------------------------------
+
+> class SingI (a :: k) where
+>   sing :: Sing a
+
+--------------------------------------------------------------------------------
+
+> class SingE (a :: k) where
+>   type Demote a :: Type
+>   fromSing :: Sing a -> Demote (Any :: k)
+
+
+> instance SingE (n :: Nat) where
+>   type Demote n = Nat
+>   fromSing SZero = Zero
+>   fromSing (SSucc n) = Succ $ fromSing n
+
+> class (SingI a, SingE a) => SingRep a
+> instance (SingI a, SingE a) => SingRep a
+
+------------------------------------------------------------------------------
+
+> data instance Sing (a :: Maybe k) :: Type where
+>   SNothing :: Sing Nothing 
+>   SJust :: SingRep a => Sing a -> Sing (Just a)
+
+> instance SingE (a :: Maybe k) where
+>   type Demote a = Maybe (Demote (Any :: k))
+>   fromSing SNothing = Nothing
+>   fromSing (SJust a) = Just (fromSing a)
+

src/singletons/Vec.idr

+data Vec : Type -> Nat -> Type where
+  VNil  : Vec a Z
+  VCons : a -> Vec a n -> Vec a (S n)
+
+v123 : Vec Int 3
+v123 = 1 `VCons` (2 `VCons` (3 `VCons` VNil))
+
+
+len : {n : Nat} -> Vec a n -> Nat
+len {n} v = n
+
+
+min' : Nat -> Nat -> Nat
+min' Z a = Z
+min' a Z = Z
+min' (S m)(S n) = S (min' m n)
+
+take : (n : Nat) -> Vec a m -> Vec a (min' n m)
+take Z VNil = VNil
+take Z (VCons x xs) = VNil
+take (S k) VNil = VNil
+take (S k) (VCons x xs) = VCons x (take k xs)
+
+
+data Fin : Nat -> Type where
+  FinZ : Fin (S n)
+  FinS : Fin n -> Fin (S n)
+
+nthFin : Fin n -> Vec a n -> a
+nthFin FinZ (VCons a _) = a
+nthFin (FinS n) (VCons _ v) = nthFin n v
+
+
+vReplicateExpl : (n : Nat) -> a -> Vec a n
+vReplicateExpl  Z     _ = VNil
+vReplicateExpl (S n) a = VCons a $ vReplicateExpl n a
+
+
+vReplicateImpl : {n : Nat} -> a -> Vec a n
+vReplicateImpl {n = Z}   _ = VNil
+vReplicateImpl {n = S k} a = VCons a $ vReplicateImpl a
+
+vZip : Vec a n -> Vec b n -> Vec (a,b) n
+vZip VNil VNil = VNil
+vZip (VCons a as) (VCons b bs) = VCons (a, b) $ vZip as bs
+
+-- vZip v123 $ vReplicateImpl False

src/singletons/Vec.lhs

+> {-# LANGUAGE RankNTypes #-}
+> {-# LANGUAGE FlexibleContexts #-}
+> {-# LANGUAGE FlexibleInstances #-}
+> {-# LANGUAGE KindSignatures #-}
+> {-# LANGUAGE DataKinds #-}
+> {-# LANGUAGE GADTs #-}
+> {-# LANGUAGE TypeOperators #-}
+> {-# LANGUAGE TypeFamilies #-}
+> {-# LANGUAGE ScopedTypeVariables #-}
+
+> import Data.Kind
+
+• A discussion and analysis of the current state of dependently typed
+  programming in Haskell
+• **singletons lib to generate new support**
+• example: database
+• proposals for future directions
+
+
+Peano nats (+ promotion):
+
+> data Nat = Zero | Succ Nat
+
+
+Size-indexed lists:
+
+> data Vec :: Type -> Nat -> Type where
+>   VNil  :: Vec a 'Zero
+>   VCons :: a -> Vec a n -> Vec a ('Succ n)
+
+
+> v123 = 1 `VCons` 2 `VCons` 3 `VCons` VNil
+
+> vHead :: Vec a (Succ n) -> a
+> vHead (VCons a _) = a
+
+----
+
+> vLength :: Vec a n -> Nat
+> vLength VNil = Zero
+> vLength (VCons a as) = Succ $ vLength as
+
+> type family (m :: Nat) :< (n :: Nat) :: Bool
+> type instance m        :< Zero     = False
+> type instance Zero     :< (Succ n) = True
+> type instance (Succ m) :< (Succ n) = m :< n
+
+> type family Min (m :: Nat) (n :: Nat) :: Nat
+> type instance Min m Zero = Zero
+> type instance Min Zero m = Zero
+> type instance Min (Succ m) (Succ n) = Succ (Min m n)
+
+ > type family min (m :: Nat) (n :: Nat) :: Nat where
+ >   Min m Zero = Zero
+ >   Min Zero m = Zero
+ >   Min (Succ m) (Succ n) = Succ (Min m n)
+
+
+< vtake :: Nat -> Vec a n -> Vec a ?
+
+< vtake :: Vec a n -> Vec a (Min n m)
+
+> data SNat :: Nat -> Type where
+>   SZero :: SNat Zero
+>   SSucc :: SNat n -> SNat (Succ n)
+
+> vtake :: SNat n -> Vec a m -> Vec a (Min n m)
+> vtake SZero      VNil       = VNil
+> vtake SZero     (VCons a v) = VNil
+> vtake (SSucc n) VNil        = VNil
+> vtake (SSucc n) (VCons a v) = a `VCons` vtake n v
+
+> data Fin :: Nat -> Type where
+>   FinZ :: Fin (Succ n)
+>   FinS :: Fin n -> Fin (Succ n)
+
+> nthFin :: Fin n -> Vec a n -> a
+> nthFin FinZ (VCons a _) = a
+> nthFin (FinS n) (VCons _ v) = nthFin n v
+
+no compilan:
+< nthFin FinZ VNil = undefined
+< nthFin (FiNS N) VNil = undefined
+
+
+> nth :: (n :< m ~ True) => SNat n -> Vec a m -> a
+> nth SZero (VCons a _) = a
+> nth (SSucc n) (VCons _ as) = nth n as
+
+--------------------------------------------------------------------------------
+Implicit Arguments
+--------------------------------------------------------------------------------
+
+
+Motivation:
+
+> vReplicateExpl :: SNat n -> a -> Vec a n
+> vReplicateExpl SZero     _ = VNil
+> vReplicateExpl (SSucc n) a = VCons a $ vReplicateExpl n a
+
+
+> vZip :: Vec a n -> Vec b n -> Vec (a,b) n
+> vZip VNil VNil = VNil
+> vZip (VCons a as) (VCons b bs) = VCons (a, b) $ vZip as bs
+
+λ> vZip v123 (vReplicateExpl (SSucc $ SSucc $ SSucc $ SZero) False)
+
+
+
+Building explicit arguments, a manopla
+
+> class SingNatI (n :: Nat) where
+>   singN :: SNat n
+
+> instance SingNatI Zero where
+>   singN = SZero
+> instance SingNatI n =>
+>   SingNatI (Succ n) where
+>   singN = SSucc singN
+
+> vReplicateImpl :: forall n a . SingNatI n => a -> Vec a n
+> vReplicateImpl a =
+>   case (singN :: SNat n) of
+>     SZero   -> VNil
+>     -- SSucc _ -> VCons a (vReplicateImpl a)
+
+
+> class Rep (n :: Nat) where
+>   rep :: a -> Vec a n
+> instance Rep Zero where
+>   rep _ = VNil
+> instance Rep n => Rep (Succ n) where 
+>   rep a = VCons a $ rep a
+
+
+SNI (S k) /=> SNI k
+--------------------------------------------------------------------------------
+FromSing
+
+> class SingNatE (n :: Nat) where
+>   fromSingN :: SNat n -> Nat
+
+> instance SingNatE (n :: Nat) where
+>   fromSingN SZero     = Zero
+>   fromSingN (SSucc n) = Succ $ fromSingN n
+
+--------------------------------------------------------------------------------
+ - Problemas?
+ - nth paper
+
+
+
+
+
+
+
+
+--------------------------------------------------------------------------------
+
+> infixr 5 `VCons`
+
+> instance Show (Vec a Zero) where show _ = "[]"
+> instance Show a => Show (Vec a (Succ Zero)) where
+>   show (VCons a _) = '[': show a ++ "]"
+> instance (Show a, Show (Vec a (Succ n)))
+>   => Show (Vec a (Succ (Succ n))) where
+>   show (VCons a v) = '[' : show a ++ ", " ++ drop 1 (show v)
+

src/singletons/VecSing.lhs

+> {-# LANGUAGE TemplateHaskell #-}
+> {-# LANGUAGE RankNTypes #-}
+> {-# LANGUAGE FlexibleContexts #-}
+> {-# LANGUAGE FlexibleInstances #-}
+> {-# LANGUAGE KindSignatures #-}
+> {-# LANGUAGE DataKinds #-}
+> {-# LANGUAGE GADTs #-}
+> {-# LANGUAGE TypeOperators #-}
+> {-# LANGUAGE TypeFamilies #-}
+> {-# LANGUAGE ScopedTypeVariables #-}
+> {-# LANGUAGE PolyKinds #-}
+> {-# LANGUAGE UndecidableInstances #-}
+
+> import Data.Kind
+> import Data.Singletons
+> import Data.Singletons.TH
+
+> data Nat = Zero | Succ Nat
+
+
+https://hackage.haskell.org/package/singletons-0.8/src/README
+
+https://github.com/goldfirere/singletons/issues/274
+
+https://ryanglscott.github.io/2019/05/26/on-the-arity-of-type-families/
+
+cambio a TF:
+https://hackage.haskell.org/package/singletons-2.6/changelog
+https://github.com/goldfirere/singletons/issues/318#issuecomment-467067257
+
+> $(genSingletons [''Nat])
+
+> $(promote [d|
+>  plus :: Nat -> Nat -> Nat
+>  plus Zero n = n
+>  plus (Succ m) n = Succ (plus m n)
+>  plus (Succ m) n = Succ (plus m n)
+>  |])

src/singletons/database/Main.hs

+{-# LANGUAGE PolyKinds, DataKinds, TemplateHaskell, TypeFamilies,
+    GADTs, TypeOperators, RankNTypes, FlexibleContexts, UndecidableInstances,
+    FlexibleInstances, ScopedTypeVariables, MultiParamTypeClasses,
+    ConstraintKinds, InstanceSigs, EmptyCase, StandaloneDeriving  #-}
+
+{- GradingClient.hs
+
+(c) Richard Eisenberg 2012
+rae@cs.brynmawr.edu
+
+This file accesses the database described in Database.hs and performs
+some basic queries on it.
+
+-}
+
+module Main where
+
+import Data.Singletons
+import Data.Singletons.TH
+import Data.Singletons.Prelude.List
+import Database
+
+$(singletons [d|
+  lastName, firstName, yearName, gradeName, majorName :: [AChar]
+  lastName = [CL, CA, CS, CT]
+  firstName = [CF, CI, CR, CS, CT]
+  yearName = [CY, CE, CA, CR]
+  gradeName = [CG, CR, CA, CD, CE]
+  majorName = [CM, CA, CJ, CO, CR]
+
+  gradingSchema :: Schema
+  gradingSchema = Sch [Attr lastName STRING,
+                       Attr firstName STRING,
+                       Attr yearName NAT,
+                       Attr gradeName NAT,
+                       Attr majorName BOOL]
+
+  names :: Schema
+  names = Sch [Attr firstName STRING,
+               Attr lastName STRING]
+  |])
+
+main :: IO ()
+main = do
+  h <- connect "grades" sGradingSchema
+  let ra = Read h
+
+  allStudents <- query $ Project sNames ra
+  putStrLn $ "Names of all students: " ++ (show allStudents) ++ "\n"
+
+  majors <- query $ Select (Element sGradingSchema sMajorName) ra
+  putStrLn $ "Students in major: " ++ (show majors) ++ "\n"
+
+  b_students <-
+    query $ Project sNames $
+            Select (LessThan (Element sGradingSchema sGradeName) (LiteralNat 90)) ra
+  putStrLn $ "Names of students with grade < 90: " ++ (show b_students) ++ "\n"

src/singletons/database/MyRow.hs

+{-# LANGUAGE PolyKinds, DataKinds, TemplateHaskell, TypeFamilies,
+    GADTs, TypeOperators, RankNTypes, FlexibleContexts, UndecidableInstances,
+    FlexibleInstances, ScopedTypeVariables, MultiParamTypeClasses,
+    ConstraintKinds, InstanceSigs, EmptyCase, StandaloneDeriving #-}
+{-# OPTIONS_GHC -Wno-warnings-deprecations #-}
+
+import GHC.TypeLits (Symbol)
+import Data.Kind (Type)
+import Data.Type.Equality
+import Data.Type.Bool
+
+data Nat = Zero | Succ Nat deriving (Eq, Read, Show)
+data Vec (a :: Type) (n :: Nat) where
+  VNil :: Vec a Zero
+  VCons :: a -> Vec a n -> Vec a (Succ n)
+
+data U = BOOL | STRING | NAT | VEC U Nat
+        deriving (Eq, Read, Show)
+
+type family El (u :: U) :: k --
+
+data Attribute = Attr Symbol U
+
+data Schema = Sch [Attribute]
+
+
+-- Hoy pueden promover las filas, a diferencia de lo que se comenta en el paper
+-- :k ('Sch '[Attr "a" BOOL, Attr "a" BOOL]) :: Schema
+-- :k (('ConsRow (El 'BOOL) ('ConsRow (El 'BOOL) ('EmptyRow '[])))
+--      :: Row (Sch '[Attr "a" BOOL,Attr "a" BOOL]))
+
+
+
+-- agregando la constraint, se puede controlar que no hayan filas repetidas,
+-- cosa que no era posible en aquel momento
+data Row :: Schema -> Type where
+  EmptyRow :: [Int] -> Row (Sch '[])
+  ConsRow :: -- (IsSet ((Attr name u) ': s) ~ True)
+    El u -> Row (Sch s) -> Row (Sch ((Attr name u) ': s))
+
+
+--------------------------------------------------------------------------------
+-- aux: predicado IsSet
+type family IsSet (s :: [Attribute]) :: Bool where
+  IsSet '[] = True
+  IsSet (Attr s u ': xs) = Not (In s xs) && IsSet xs
+
+type family In (x :: Symbol) (xs :: [Attribute]) :: Bool where
+  In x '[] = False
+  In x (Attr h u ': xs) = (x == h) || In x xs

src/singletons/database/grades.dat

+"Takei"
+"George"
+2015
+92
+True
+"Hwang"
+"Lisa"
+2017
+97
+False
+"Gupta"
+"Laksh"
+2016
+94
+True
+"Smythe"
+"John"
+2017
+88
+False
+"Klein"
+"Nadine"
+2016
+86
+True
\ No newline at end of file

src/singletons/database/grades.schema

+STRING
+STRING
+NAT
+NAT
+BOOL