Skip to content

Instantly share code, notes, and snippets.

@SimonHauguel

SimonHauguel/Math_Expression_Validity_CompileTime.hs

Created May 13, 2021 19:34
Show Gist options
  • Save SimonHauguel/c93f3009a3a3775d378cca40551f379b to your computer and use it in GitHub Desktop.
Save SimonHauguel/c93f3009a3a3775d378cca40551f379b to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Math_Expression_Validity_CompileTime.hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
import Data.Kind ( Type )
-- Z 'Set'
data Z :: Type where
P :: Z -> Z -- Predecessor Function
S :: Z -> Z -- Successor Function
O :: Z -- The Value 0
-- List representation of mathematical expression
data List
:: Z -- If parenthesis are balanced == 0
-> Z -- If it's a valid expression == 1
-> Type where
Nil :: List 'O 'O -- Empty List
PRToken :: forall (x :: Z). List x 'O -> List ('S x) 'O -- Right Parenthesis
-- A right parenthesis can be placed iff the right expression is a null-value expression (ie : OP Val; OP Val OP Val...)
PLToken :: forall (x :: Z). List ('S x) ('S 'O) -> List x ('S 'O) -- Left Parenthesis
-- A left parenthesis can be placed iff the right expression is an one-value expression (ie : Val Op Val; Val Op Val Op Val...)
OPCons :: forall (x :: Z). Char -> List x ('S 'O) -> List x 'O -- Operator
-- An operator can be placed online before a number or a left-parenthesis
LiCons :: forall (x :: Z). Int -> List x 'O -> List x ('S 'O) -- Number
-- A number can be placed online after an operator
type CorrectExpr = List 'O ('S 'O) -- Why ('S 'O) ? Because a valid expression contain one more number than operator
-- | -- ie : 1 + 2 (2 N, 1 OP); 1 + 2 + 3 (3 N, 2 OP) ; 1 - 2 + 3 - 4 (4 N, 3 OP)...
-- |
-- --> Balanced parenthesis
-- Let's check
a1 :: CorrectExpr
a1 = LiCons 1 $ OPCons '+' $ LiCons 2 Nil
-- 1 + 2
-- Valid
{-
a2 :: CorrectExpr
a2 = OPCons '+' $ LiCons 2 Nil
+ 2
Invalid
• Couldn't match type ‘'O’ with ‘'S 'O’
Expected type: CorrectExpr
Actual type: List 'O 'O
-}
a3 :: CorrectExpr
a3 = PLToken $ LiCons 2 $ OPCons '+' $ LiCons 1 $ PRToken Nil
-- ( 2 + 1 )
-- Valid
{-
a4 :: CorrectExpr
a4 = LiCons 2 (OPCons '+' (LiCons 1 (PRToken Nil)))
2 + 1 )
Invalid
• Couldn't match type ‘'S 'O’ with ‘'O’
Expected type: CorrectExpr
Actual type: List ('S 'O) ('S 'O)
-}
a5 :: CorrectExpr
a5 = PLToken $ PLToken $ LiCons 2 $ OPCons '+' $ LiCons 1 $ PRToken $ PRToken Nil
-- ( ( 2 + 1 ) )
-- Valid
{-
a6 :: CorrectExpr
a6 = LiCons 2 $ LiCons 1 $ OPCons '+' Nil
2 1 +
Invalid
• Couldn't match type ‘'S 'O’ with ‘'O’
Expected type: List 'O 'O
Actual type: List 'O ('S 'O)
• Couldn't match type ‘'O’ with ‘'S 'O’
Expected type: List 'O ('S 'O)
Actual type: List 'O 'O
-}
{-
a7 :: CorrectExpr
a7 = PRToken $ LiCons 1 $ OPCons '+' $ PLToken $ LiCons 2 $ Nil
( 1 + ) 2
Invalid
• Couldn't match type ‘'S x0’ with ‘'O’
Expected type: CorrectExpr
Actual type: List ('S x0) 'O
• Couldn't match type ‘'S 'O’ with ‘'O’
Expected type: List x0 'O
Actual type: List x0 ('S 'O)
• Couldn't match type ‘'O’ with ‘'S x0’
Expected type: List ('S x0) ('S 'O)
Actual type: List 'O ('S 'O)
-}
{-
a8 :: CorrectExpr
a8 = LiCons 1 $ PRToken $ OPCons '+' $ LiCons 2 $ PLToken $ Nil
1 ( + 2 )
Invalid
• Couldn't match type ‘'S x0’ with ‘'O’
Expected type: CorrectExpr
Actual type: List ('S x0) ('S 'O)
• Couldn't match type ‘'S 'O’ with ‘'O’
Expected type: List x0 'O
Actual type: List x0 ('S 'O)
• Couldn't match type ‘'O’ with ‘'S x0’
Expected type: List ('S x0) ('S 'O)
Actual type: List 'O 'O
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment